Add incr_twice.imp

SoftwareFoundationGroupAtKyotoU · Jan 30, 2024 · dc1da24 · dc1da24
1 parent 9491572
commit dc1da24
Showing 1 changed file with 16 additions and 0 deletions.
diff --git a/src/concurrency/flow/negative/not-supported/incr_twice.imp b/src/concurrency/flow/negative/not-supported/incr_twice.imp
@@ -0,0 +1,16 @@
+{
+    let a = mkref 2 in
+    let l = newlock() in
+    let t = fork({
+        acq(l);
+        a := *a + 1;
+        rel(l);
+    }) in {
+        acq(l);
+        a := *a + 1;
+        rel(l);
+        wait(t);
+        freelock(l);
+        assert(*a = 4);
+    }
+}