Initial operational semantics artifact for Rio

semantics/dune

@@ -0,0 +1,3 @@
+(env
+  (dev
+    (flags (:standard -w -27-32-69 -warn-error -a))))

semantics/dune-project

@@ -0,0 +1,24 @@
+(lang dune 3.16)
+
+(name semantics)
+
+(generate_opam_files true)
+
+(source
+ (github cucapra/packet-scheduling))
+
+(authors "Kabir Samsi")
+
+(maintainers "Kabir Samsi")
+
+(license LICENSE)
+
+(documentation https://github.com/cucapra/packet-scheduling/discussions/67)
+
+(package
+ (name semantics)
+ (synopsis "OCaml artifact of the operational semantics construct for Rio")
+ (description "TBD")
+ (depends ocaml dune)
+ (allow_empty)
+)

semantics/lib/dune

@@ -0,0 +1,3 @@
+(library
+ (name semantics)
+ (modules_without_implementation packet queue))

semantics/lib/packet.mli

@@ -0,0 +1,14 @@
+(** A signature for packets. *)
+
+module type Packet = sig
+  type t
+
+  (* rank pkt is the rank of pkt *)
+  val rank : t -> float
+
+  (* time pkt is the pop deadline of pkt *)
+  val time : t -> float
+
+  (* weight pkt is the weight pkt *)
+  val weight : t -> float
+end

semantics/lib/queue.mli

@@ -0,0 +1,21 @@
+(** A signature for queues. *)
+
+module type Queue = sig
+  (* An abstract type for a queue with elements of type 'a *)
+  type 'a t
+
+  (* empty is the empty queue *)
+  val empty : 'a t
+
+  (* push pushes the latest element (with some rank) into the queue *)
+  val push : 'a * 'a t -> 'a t
+
+  (* pop qs returns the highest-priority element (if there is one) and modified queue *)
+  val pop : 'a t -> 'a option * 'a t
+
+  (* update qs q q' is qs[q'/q] *)
+  val update : 'a t list -> 'a t -> 'a t -> 'a t list
+
+  (* flush q returns all elements enqeued in q. *)
+  val flush : 'a t -> 'a list
+end

semantics/lib/semantics.ml

@@ -0,0 +1,50 @@
+open Packet
+open Queue
+
+(** 
+  Implementation of the operational semantics discussed in #67 (see linked documentation)
+*)
+
+(** A signature for semantics. *)
+module type SemanticsSig = sig
+  type prog
+  type pkt
+  type queue
+  type state
+
+  exception EvaluationError
+
+  val push : pkt * queue * state -> state
+  (** push pkt q st enqueues pkt to the queue q, and updates st. *)
+
+  val pop : state -> pkt option * state
+  (* pop st dequeues the next packet in line, and updates st. *)
+end
+
+(** An implementation for semantics. *)
+module Semantics (Pkt : Packet) (Q : Queue) : SemanticsSig = struct
+  (* For the time being, we operate in a world without variables. *)
+  type clss = string
+  type set = Class of clss | Union of set list
+
+  exception EvaluationError
+
+  type stream =
+    | Fifo of set
+    | EarliestDeadline of set
+    | ShortestJobNext of set
+    | RoundRobin of stream list
+    | Strict of stream list
+    | WeightedFair of stream list * int list
+
+  type prog = stream
+  type pkt = Pkt.t
+  type queue = pkt Q.t
+  type state = prog * queue list
+
+  let push (pkt, q, (p, qs)) =
+    if List.mem q qs then (p, Q.update qs q (Q.push (pkt, q)))
+    else raise EvaluationError
+
+  let pop = failwith "TODO"
+end

semantics/semantics.opam

@@ -0,0 +1,30 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "OCaml artifact of the operational semantics construct for Rio"
+description: "TBD"
+maintainer: ["Kabir Samsi"]
+authors: ["Kabir Samsi"]
+license: "LICENSE"
+homepage: "https://github.com/cucapra/packet-scheduling"
+doc: "https://github.com/cucapra/packet-scheduling/discussions/67"
+bug-reports: "https://github.com/cucapra/packet-scheduling/issues"
+depends: [
+  "ocaml"
+  "dune" {>= "3.16"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/cucapra/packet-scheduling.git"