diff --git a/src/concurrency/flow/positive/counter.imp b/src/concurrency/flow/positive/counter.imp
index 7bcd6802..d07ad483 100644
--- a/src/concurrency/flow/positive/counter.imp
+++ b/src/concurrency/flow/positive/counter.imp
@@ -1,43 +1,77 @@
-incr(x, max, l) {
+// Increment `x` while satisfying `x <= max`
+incr(x, min_max, l) {
     acq(l);
-    assert(*x <= max);
+    check(x, min_max);
+    let (_, max) = min_max in
     if *x < max then {
         x := *x + 1;
-        assert(*x <= max);
+        check(x, min_max);
         rel(l);
     } else {
         rel(l);
-        incr(x, max, l);
+        incr(x, min_max, l);
+    }
+}
+
+// Increment `x` nondeterminstic times
+repeat_incr(x, min_max, l) {
+    if _ then ()
+    else {
+        incr(x, min_max, l);
+        repeat_incr(x, min_max, l)
     }
 }
 
-decr(x, min, l) {
+// Decrement `x` while satisfying `min <= x`
+decr(x, min_max, l) {
     acq(l);
-    assert(min <= *x);
+    check(x, min_max);
+    let (min, _) = min_max in
     if min < *x then {
         x := *x - 1;
-        assert(min <= *x);
+        check(x, min_max);
         rel(l);
     } else {
         rel(l);
-        decr(x, min, l);
+        decr(x, min_max, l);
+    }
+}
+
+// Decrement `x` nondeterminstic times
+repeat_decr(x, min_max, l) {
+    if _ then ()
+    else {
+        decr(x, min_max, l);
+        repeat_decr(x, min_max, l)
     }
 }
 
+check(x, min_max) {
+    let (min, max) = min_max in {
+        assert(min <= *x);
+        assert(*x <= max);
+    }
+}
+
+// Limited Counter:
+// Repeat increment and decrement the counter nondeterministic times
+// while keeping the value between `min` and `max`.
 {
-    let min = 0 in
-    let max = 2 in
-    let x = mkref min in
-    let l = newlock() in
-    let t = fork({
-        decr(x, min, l);
-        decr(x, min, l);
-        decr(x, min, l);
-    }) in {
-        incr(x, max, l);
-        incr(x, max, l);
-        incr(x, max, l);
-        wait(t);
-        freelock(l)
+    let min = (_: ~ >= 0) in
+    let max = (_: ~ >= min) in
+    let min_max = (min, max) in
+    let counter = mkref min in {
+        check(counter, min_max);
+        let l = newlock() in
+        let t = fork({
+            repeat_decr(counter, min_max, l);
+        }) in {
+            repeat_incr(counter, min_max, l);
+
+            wait(t);
+            freelock(l);
+            
+            check(counter, min_max);
+        }
     }
 }
diff --git a/src/concurrency/flow/positive/counter2.imp b/src/concurrency/flow/positive/counter2.imp
new file mode 100644
index 00000000..7bcd6802
--- /dev/null
+++ b/src/concurrency/flow/positive/counter2.imp
@@ -0,0 +1,43 @@
+incr(x, max, l) {
+    acq(l);
+    assert(*x <= max);
+    if *x < max then {
+        x := *x + 1;
+        assert(*x <= max);
+        rel(l);
+    } else {
+        rel(l);
+        incr(x, max, l);
+    }
+}
+
+decr(x, min, l) {
+    acq(l);
+    assert(min <= *x);
+    if min < *x then {
+        x := *x - 1;
+        assert(min <= *x);
+        rel(l);
+    } else {
+        rel(l);
+        decr(x, min, l);
+    }
+}
+
+{
+    let min = 0 in
+    let max = 2 in
+    let x = mkref min in
+    let l = newlock() in
+    let t = fork({
+        decr(x, min, l);
+        decr(x, min, l);
+        decr(x, min, l);
+    }) in {
+        incr(x, max, l);
+        incr(x, max, l);
+        incr(x, max, l);
+        wait(t);
+        freelock(l)
+    }
+}
diff --git a/src/concurrency/flow/positive/queue.imp b/src/concurrency/flow/positive/queue.imp
index 877d88dd..e7ef21c0 100644
--- a/src/concurrency/flow/positive/queue.imp
+++ b/src/concurrency/flow/positive/queue.imp
@@ -98,19 +98,32 @@ pop(q, l) {
   }
 }
 
+repeat_push(q, l) {
+  if _ then ()
+  else {
+      push(q, _, l);
+      repeat_push(q, l)
+  }
+}
+
+repeat_pop(q, l) {
+  if _ then ()
+  else {
+      push(q, _, l);
+      repeat_push(q, l)
+  }
+}
+
 {
-  let q = mkqueue(2) in
+  let n = (_: ~ > 0) in
+  let q = mkqueue(n) in
   let l = newlock() in
   let t = fork({
-    push(q, _, l);
-    push(q, _, l);
-    push(q, _, l);
+    repeat_push(q, l);
   }) in {
-    pop(q, l);
-    pop(q, l);
-    pop(q, l);
+    repeat_pop(q, l);
     wait(t);
     freelock(l);
-    check(q)
+    check(q);
   }
 }
diff --git a/src/concurrency/flow/positive/repeated_counter.imp b/src/concurrency/flow/positive/repeated_counter.imp
deleted file mode 100644
index 63e6a3fc..00000000
--- a/src/concurrency/flow/positive/repeated_counter.imp
+++ /dev/null
@@ -1,77 +0,0 @@
-// Increment `x` while satisfying `x <= max`
-incr(x, min_max, l) {
-    acq(l);
-    check(x, min_max);
-    let (_, max) = min_max in
-    if *x < max then {
-        x := *x + 1;
-        check(x, min_max);
-        rel(l);
-    } else {
-        rel(l);
-        incr(x, min_max, l);
-    }
-}
-
-// Increment `x` nondeterminstic times
-repeat_incr(x, min_max, l) {
-    if _ then ()
-    else {
-        incr(x, min_max, l);
-        repeat_incr(x, min_max, l)
-    }
-}
-
-// Decrement `x` while satisfying `min <= x`
-decr(x, min_max, l) {
-    acq(l);
-    check(x, min_max);
-    let (min, _) = min_max in
-    if min < *x then {
-        x := *x - 1;
-        check(x, min_max);
-        rel(l);
-    } else {
-        rel(l);
-        decr(x, min_max, l);
-    }
-}
-
-// Decrement `x` nondeterminstic times
-repeat_decr(x, min_max, l) {
-    if _ then ()
-    else {
-        decr(x, min_max, l);
-        repeat_decr(x, min_max, l)
-    }
-}
-
-check(x, min_max) {
-    let (min, max) = min_max in {
-        assert(min <= *x);
-        assert(*x <= max);
-    }
-}
-
-// Limited Counter:
-// Repeat increment and decrement nondeterministic times
-// while keeping the counter value between `min` and `max`.
-{
-    let min = (_: ~ >= 0) in
-    let max = (_: ~ >= min) in
-    let min_max = (min, max) in
-    let counter = mkref min in {
-        check(counter, min_max);
-        let l = newlock() in
-        let t = fork({
-            repeat_decr(counter, min_max, l);
-        }) in {
-            repeat_incr(counter, min_max, l);
-
-            wait(t);
-            freelock(l);
-            
-            check(counter, min_max);
-        }
-    }
-}
diff --git a/src/concurrency/flow/positive/wip/return_lock.imp b/src/concurrency/flow/positive/wip/return_lock.imp
new file mode 100644
index 00000000..0cc65c4b
--- /dev/null
+++ b/src/concurrency/flow/positive/wip/return_lock.imp
@@ -0,0 +1,29 @@
+create(init){
+    let x = mkref init in
+    let l = newlock() in
+    (x, l) 
+}
+
+blocking_update(xl, y) {
+    let (x, l) = xl in {
+        acq(l);
+        x := y;
+        rel(l);
+        alias(xl.0 = x);
+        alias(xl.1 = l);
+    }
+}
+
+{
+    let xl = create(3) in
+    let t = fork(
+        blocking_update(xl, 2)
+    ) in {
+        blocking_update(xl, 4);
+        wait(t);
+        let (x, l) = xl in {
+            freelock(l);
+            assert(*x > 0);
+        }
+    }
+}
diff --git a/src/concurrency/ownership/negative/racial_write.imp b/src/concurrency/ownership/negative/racy_write.imp
similarity index 100%
rename from src/concurrency/ownership/negative/racial_write.imp
rename to src/concurrency/ownership/negative/racy_write.imp
diff --git a/src/concurrency/ownership/negative/racial_write2.imp b/src/concurrency/ownership/negative/racy_write2.imp
similarity index 100%
rename from src/concurrency/ownership/negative/racial_write2.imp
rename to src/concurrency/ownership/negative/racy_write2.imp