Skip to content

Commit

Permalink
Make programs testable via semantic rules
Browse files Browse the repository at this point in the history
  • Loading branch information
KabirSamsi committed Oct 25, 2024
1 parent a307368 commit 89ca907
Show file tree
Hide file tree
Showing 3 changed files with 27 additions and 19 deletions.
17 changes: 17 additions & 0 deletions semantics/lib/program.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
(** A module representation for Rio program forms. *)
module Program = struct
type clss = string
type set = Class of clss | Union of set list

type stream =
(* Set To Stream *)
| Fifo of set
| EarliestDeadline of set
| ShortestJobNext of set
(* Stream To Stream *)
| RoundRobin of stream list
| Strict of stream list
| WeightedFair of stream list * int list

type prog = stream (* Exportable type *)
end
28 changes: 9 additions & 19 deletions semantics/lib/semantics.ml
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
open Packet
open Queue
open Program

(** Implementation of the semantics discussed in #67. See linked documentation. *)

Expand All @@ -22,26 +23,14 @@ end
(** An implementation for Rio's operational semantics. *)
module Semantics (Pkt : Packet) (Q : Queue with type elt = Pkt.t) :
SemanticsSig = struct
type clss = string
type set = Class of clss | Union of set list

exception EvaluationError

type stream =
(* Set To Stream *)
| Fifo of set
| EarliestDeadline of set
| ShortestJobNext of set
(* Stream To Stream *)
| RoundRobin of stream list
| Strict of stream list
| WeightedFair of stream list * int list

type prog = stream
type set = Program.set
type prog = Program.prog
type pkt = Pkt.t
type queue = Q.t
type state = prog * queue list

exception EvaluationError

let push (pkt, q, (p, qs)) =
(* Assert that the relevant queue is part of the larger list of queues *)
if List.mem q qs then (p, Q.update q (Q.push (pkt, q)) qs)
Expand Down Expand Up @@ -82,8 +71,9 @@ module Semantics (Pkt : Packet) (Q : Queue with type elt = Pkt.t) :
(pkt, (p, qs_new))

(* Compute the number of subclasses in a program *)
let rec num_classes prog =
let rec n_classes_set = function
let rec num_classes (prog : prog) =
let rec n_classes_set (set : set) =
match set with
| Class _ -> 1
| Union lst -> List.fold_right (fun x acc -> n_classes_set x + acc) lst 0
in
Expand All @@ -109,7 +99,7 @@ module Semantics (Pkt : Packet) (Q : Queue with type elt = Pkt.t) :
| h :: t ->
if idx = 0 then newval :: t else h :: update_i (idx - 1) newval t

let rec pop (p, qs) =
let rec pop ((p : prog), qs) =
match p with
(* FIFO pops the packet with the lowest rank *)
| Fifo _ -> pop_set_stream Pkt.rank (p, qs)
Expand Down
1 change: 1 addition & 0 deletions semantics/test/test_semantics.ml
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
open SemanticsImpl.Packet
open SemanticsImpl.Queue
open SemanticsImpl.Semantics
open SemanticsImpl.Program
open OUnit2

module PacketImpl : Packet = struct
Expand Down

0 comments on commit 89ca907

Please sign in to comment.