Add example programs using condition variables from pldi23

.gitignore

@@ -1,6 +1,7 @@
 *~
 primlc
 priml/c72s
+_opam/
 *.swp
 *.swo
 millet.toml

priml-examples/Makefile

@@ -67,5 +67,14 @@ fib_term: fib_term.prm
 web: web-src/web.prm
 	$(PRIML) web-src/web.prm web
 
+cv_prod_cons: cv-prod-cons-correct.prm
+	$(PRIML) cv-prod-cons-correct.prm cv_prod_cons
+
+cv_prod_cons_err: cv-prod-cons-err.prm
+	$(PRIML) cv-prod-cons-err.prm cv_prod_cons_err
+
+cv_inversion_err: cv-inversion-err.prm
+	$(PRIML) cv-inversion-err.prm cv_inversion_err
+
 clean:
-	rm -f bank email fibserv fibserv-fair fib_term web
+	rm -f bank email fibserv fibserv-fair fib_term web cv_inversion_err cv_prod_cons_err cv_prod_cons

priml-examples/cv-inversion-err.prm

@@ -0,0 +1,45 @@
+(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
+ * simple priority inversion example
+ * ---
+ *
+ * shows how the PriML compiler will raise a type error if passing a condition
+ * variable causes a priority inversion.
+ *
+ * code translated from the C-family example (Fig. 2) given in _pldi23_:
+ *
+ * ```
+ * void <Low>f(CV<High> cv, int *result) {
+ *   ...
+ *   *result = ...;
+ *   signal(cv); //ill-typed
+ * }
+ *
+ * void <High>main() {
+ *   CV<High> cv = new CV<High>();
+ *   int result = 0;
+ *   spawn<Low>(f(CV, &result));
+ *   ...
+ *   wait(cv);
+ * }
+ * ```
+ * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)
+
+priority high
+priority low
+order low < high
+
+fun foo cv res =
+    let val _ =
+        res := !res + 1
+    in
+        cmd {
+            signal cv (* ill-typed *)
+        }
+    end
+
+main {
+    cv <- newcv[high];
+    res <- ref 1;
+    t <- spawn[low] { foo cv res };
+    sync t
+}

priml-examples/cv-prod-cons-correct.prm

@@ -0,0 +1,99 @@
+(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
+ * producer consumer example
+ * ---
+ *
+ * description quoted & code translated from the C-family example (Fig. 4)
+ * given in _pldi23_:
+ *
+ * > The producer-consumer example, without type errors or priority inversions
+ *
+ * ```
+ * void <High>prod(CV<Low> cv, Buffer *buf){
+ *   while(true) {
+ *     ...
+ *     append(buf, x);
+ *     signal(cv);
+ *   }
+ * }
+ * 
+ * void <High>cons(CV<High> cv, Buffer *buf){
+ *   while(true) {
+ *     if empty(buffer){
+ *       wait(cv);
+ *     }
+ *     x = pop(buf);
+ *     ...
+ *   }
+ * }
+ * 
+ * void <Low>main(){
+ *   CV<Low>cv = new CV();
+ *   Buffer *buf;
+ *   
+ *   spawn<High>(prod(cv, buf));
+ *   CV<High> cv2 = promote<High>(cv);
+ *   // Would now be ill-typed to spawn prod
+ *   spawn<High>(cons(cv, buf));
+ * }
+ * ```
+ * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)
+
+priority high
+priority low
+order low < high
+
+(* prod
+ * ---
+ *
+ * increments a number and pushes it to a queue, then signals before looping
+ *)
+(* fun prod (cv: cv[low]) (queue: int list ref) = *)
+fun prod cv queue =
+    let fun loop c q n =
+        let val _ =
+            q := n :: !q
+        in
+            cmd {
+                signal cv;
+                loop cv queue (n + 1)
+            }
+        end
+    in
+        loop cv queue 1
+    end
+
+(* cons
+ * ---
+ *
+ * if queue is empty, waits for signal before looping;
+ * otherwise pops top item & prints that it was received before looping
+ *)
+(* fun cons (cv: cv[high]) (queue: ref int list) = *)
+fun cons cv queue =
+    let fun loop c q =
+        case q of
+            nil    => 
+                cmd {
+                    wait cv;
+                    loop c q
+                }
+          | x::xs =>
+                loop c q
+    in
+        loop cv queue
+    end
+
+(* main
+ * ---
+ *
+ * initializes cv & queue, then spawns prod & cons threads.
+ *)
+main {
+    cv <- newcv[low];
+    queue <- ref nil;
+    p <- spawn[high] { prod cv queue };
+    cv2 <- promote[high] cv;
+    (* would now be ill-typed to spawn prod *)
+    c <- spawn[high] { cons cv2 queue };
+    sync c
+}

priml-examples/cv-prod-cons-err.prm

@@ -0,0 +1,97 @@
+(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
+ * producer consumer priority inversion error example
+ * ---
+ *
+ * description quoted & code translated from the C-family example (Fig. 3)
+ * given in _pldi23_:
+ *
+ * > Initial attempt at the producer-consumer program, which has a priority
+ * > inversion (and a type error, in our full system)
+ *
+ * ```
+ * void <High>prod(CV<High> cv, Buffer *buf){
+ *   while(true) {
+ *     ...
+ *     append(buf, x);
+ *     signal(cv);
+ *   }
+ * }
+ * 
+ * void <High>cons(CV<High> cv, Buffer *buf){
+ *   while(true) {
+ *     if empty(buffer){
+ *       wait(cv);
+ *     }
+ *     x = pop(buf);
+ *     ...
+ *   }
+ * }
+ * 
+ * void <Low>main(){
+ *   CV<High>cv = new CV();
+ *   Buffer *buf;
+ *   
+ *   spawn<High>(cons(cv, buf));
+ *   spawn<High>(prod(cv, buf)); // ill-typed
+ * }
+ * ```
+ * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)
+
+priority high
+priority low
+order low < high
+
+(* prod
+ * ---
+ *
+ * increments a number and pushes it to a queue, then signals before looping
+ *)
+(* fun prod (cv: cv[high]) (queue: int list ref) = *)
+fun prod cv queue =
+    let fun loop c q n =
+        let val _ =
+            q := n :: !q
+        in
+            cmd {
+                signal cv;
+                loop cv queue (n + 1)
+            }
+        end
+    in
+        loop cv queue 1
+    end
+
+(* cons
+ * ---
+ *
+ * if queue is empty, waits for signal before looping;
+ * otherwise pops top item & prints that it was received before looping
+ *)
+(* fun cons (cv: cv[high]) (queue: ref int list) = *)
+fun cons cv queue =
+    let fun loop c q =
+        case q of
+            nil    => 
+                cmd {
+                    wait cv;
+                    loop c q
+                }
+          | x::xs =>
+                loop c q
+    in
+        loop cv queue
+    end
+
+(* main
+ * ---
+ *
+ * initializes cv & queue, then spawns prod & cons threads.
+ * contains priority inversion.
+ *)
+main {
+    cv <- newcv[high];
+    queue <- ref nil;
+    c <- spawn[high] { cons cv queue };
+    p <- spawn[high] { prod cv queue }; (* ill-typed *)
+    sync p
+}