From 94915729d9ddd24ea1004a2eefb714abaa8b3c9c Mon Sep 17 00:00:00 2001 From: Junya Hirashima Date: Tue, 30 Jan 2024 16:48:01 +0900 Subject: [PATCH] Fix testfile --- src/concurrency/flow/positive/counter.imp | 78 +++++++++++++------ src/concurrency/flow/positive/counter2.imp | 43 ++++++++++ src/concurrency/flow/positive/queue.imp | 29 +++++-- .../flow/positive/repeated_counter.imp | 77 ------------------ .../flow/positive/wip/return_lock.imp | 29 +++++++ .../{racial_write.imp => racy_write.imp} | 0 .../{racial_write2.imp => racy_write2.imp} | 0 7 files changed, 149 insertions(+), 107 deletions(-) create mode 100644 src/concurrency/flow/positive/counter2.imp delete mode 100644 src/concurrency/flow/positive/repeated_counter.imp create mode 100644 src/concurrency/flow/positive/wip/return_lock.imp rename src/concurrency/ownership/negative/{racial_write.imp => racy_write.imp} (100%) rename src/concurrency/ownership/negative/{racial_write2.imp => racy_write2.imp} (100%) 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