From 93587ef55bed65173889d1e880fd3f063d2cb60f Mon Sep 17 00:00:00 2001 From: Ekanshdeep Gupta Date: Thu, 21 Nov 2024 23:07:09 -0500 Subject: [PATCH] Bumped up version, updated documentation, fixed many of the tests --- README.md | 109 ++- lib/config/config.ml | 2 +- test/comparison/arc_atomics.rav | 4 +- test/comparison/inc_dec.rav | 10 +- .../comparison/{lclist.rav => lclist_wip.rav} | 0 test/comparison/peterson.rav | 192 ++--- test/concurrent/lock/spin-lock_compact.rav | 65 ++ ... ticket-lock_program_failing_no-proof.rav} | 0 test/concurrent/templates/give-up-lock.rav | 665 ------------------ .../concurrent/templates/give-up-lock_wip.rav | 235 +++++++ .../templates/single-node-compact.rav | 245 ------- .../templates/single-node-test copy.rav | 342 --------- .../concurrent/templates/single-node-test.rav | 340 --------- ...ingle-node_working.rav => single-node.rav} | 0 test/concurrent/templates/single-node.t | 2 + .../templates/single-node_annoted.rav | 426 ----------- .../templates/single-node_imports.rav | 304 -------- .../templates/single-node_rough.rav | 282 -------- .../templates/single-node_working.t | 2 - .../treiber_stack/treiber_stack_rewritten.rav | 2 +- test/iterated-star/binary-graph.rav | 59 -- test/iterated-star/binary-graph2.rav | 54 -- test/iterated-star/receiver-expr.rav | 36 - .../list_predicates2_wip.rav} | 0 .../list_predicates_wip.rav} | 0 todo.md | 29 +- 26 files changed, 525 insertions(+), 2880 deletions(-) rename test/comparison/{lclist.rav => lclist_wip.rav} (100%) create mode 100644 test/concurrent/lock/spin-lock_compact.rav rename test/concurrent/lock/{ticket-lock_program_no-proof.rav => ticket-lock_program_failing_no-proof.rav} (100%) delete mode 100644 test/concurrent/templates/give-up-lock.rav create mode 100644 test/concurrent/templates/give-up-lock_wip.rav delete mode 100644 test/concurrent/templates/single-node-compact.rav delete mode 100644 test/concurrent/templates/single-node-test copy.rav delete mode 100644 test/concurrent/templates/single-node-test.rav rename test/concurrent/templates/{single-node_working.rav => single-node.rav} (100%) create mode 100644 test/concurrent/templates/single-node.t delete mode 100644 test/concurrent/templates/single-node_annoted.rav delete mode 100644 test/concurrent/templates/single-node_imports.rav delete mode 100644 test/concurrent/templates/single-node_rough.rav delete mode 100644 test/concurrent/templates/single-node_working.t delete mode 100644 test/iterated-star/binary-graph.rav delete mode 100644 test/iterated-star/binary-graph2.rav delete mode 100644 test/iterated-star/receiver-expr.rav rename test/{list_predicates2.rav => linked-lists/list_predicates2_wip.rav} (100%) rename test/{list_predicates.rav => linked-lists/list_predicates_wip.rav} (100%) diff --git a/README.md b/README.md index c6826ad..865b392 100644 --- a/README.md +++ b/README.md @@ -1,11 +1,114 @@ # Raven -![Version 0.1 pre](https://img.shields.io/badge/version-0.1_pre-green.svg) +![Version 1.0](https://img.shields.io/badge/version-1.0-green.svg) [![MIT licensed](https://img.shields.io/badge/license-MIT-blue.svg)](https://raw.githubusercontent.com/nyu-acsys/raven/master/LICENSE) [![Builds, tests & co](https://github.com/nyu-acsys/raven/actions/workflows/ci.yml/badge.svg?branch=dev)](https://github.com/nyu-acsys/raven/actions/workflows/ci.yml) -The Resource Algebra Verification ENgine. +Raven (Resource Algebra Verification ENgine) is an SMT-based deductive verifier for concurrent separation logic. Raven supports features like invariants, custom user-defined resource algebras ("monoids"), and a powerful higher-order module system that enables code and proof re-use. Raven also has smart heuristics that automate many low-level details, and an inlined style of development that interleaves code and proof. This streamlines the process of co-developing a program alongside its proof of correctness. -Link to the Google Doc: https://docs.google.com/document/d/1AvU88AoWAMsv9lBCK980P7-cjkXOWbE_DJupAi3tK6c/edit?usp=sharing +Raven provides a highly-automated, user-friendly front-end that draws heavily from projects like [Dafny](https://github.com/dafny-lang/dafny) and [Viper](https://www.pm.inf.ethz.ch/research/viper.html). Raven has a sizeable, and growing [collection](test/concurrent) of verified implementations of fine-grained concurrent data structures commonly found in the literature and as well as real systems. +These implementations are then translated to first-order logic and passed to the [Z3](https://github.com/Z3Prover/z3) SMT-solver to determine whether the user-provided input verifies successfully. + +Raven also ships with a [library](lib/library/resource_algebra.rav) of standard resource algebra implementations, as well as higher-order resource algebra constructors that embody commonly occuring patterns in proofs of concurrent data structures. This helps the user get started with proofs quickly. + +Raven's underlying separation logic is based on the [Iris](https://iris-project.org/) separation logic framework. We vastly simplify the Iris logic by carefully restricting its most higher-order features (like impredicativity and step-indexing). This results in a sufficiently expressive logic that is amenable to robust SMT-based automation. Developing a formal proof of Raven's compatibility with Iris is part of ongoing-work. + +## Installation +Raven can be installed by running the following sequence of commmands. It requires [opam](https://opam.ocaml.org/). +``` +$ git clone https://github.com/nyu-acsys/raven.git +$ cd ./raven +$ opam switch create raven 5.2.0 +$ opam switch raven +$ opam install . --deps +$ dune build; dune install; dune runtest +``` + +## Examples +Several examples can be found in the [test](test) folder. The [ci](test/ci) folder contains many small example that can be used to learn Raven syntax for specific features. Complete verified implementations of concurrent data structures can be found in the [concurrent](test/concurrent) folder. Here are a few notable ones to get started, in roughly increasing order of complexity: +1. [spin_lock](test/concurrent/lock/spin-lock.rav) +1. [monotonic_counter](test/concurrent/counter/counter_monotonic.rav) +1. [treiber_stack](test/concurrent/treiber_stack/treiber_stack_atomics.rav) +1. [atomic_resource_counter](test/comparison/arc_atomics.rav) +1. [bplustree](test/concurrent/templates/bplustree.rav) +1. [give-up template](test/concurrent/templates/give-up.rav) + +## Usage +Raven can be executed on a file `test/concurrent/treiber_stack/treiber_stack_atomics.rav` as follows: +``` +$ raven test/concurrent/treiber_stack/treiber_stack_atomics.rav +Raven version 1.0 +Verification successful. +``` +Here is a failing example: +``` +$ raven test/ci/back-end/fail/fpu_fail.rav +Raven version 1. +[Error] File "test/ci/back-end/fail/fpu_fail.rav", line 7, columns 2-14: +7 | fpu(x.f, 4); + ^^^^^^^^^^^^ +Verification Error: This update may not be frame-preserving. +``` + +### Raven Manual +``` +RAVEN(1) Raven Manual RAVEN(1) + +NAME + raven + +SYNOPSIS + raven [OPTION]… [INPUT]… + +ARGUMENTS + INPUT + Input file. + +OPTIONS + --color=WHEN (absent=auto) + Colorize the output. WHEN must be one of auto, always or never. + + --lsp-mode + Format error messages for LSP integration. + + --nostdlib + Skip standard library. + + -q, --quiet + Be quiet. Takes over -v and --verbosity. + + --shh + Suppress greeting. + + --smt-info + Let Z3 produce diagostic output. + + --smt-timeout=VAL (absent=10000) + Timeout for SMT solver in ms. + + --stats + Output only program stats: concrete instruction steps, ghost + instruction steps, and number of specification formulae + + --typeonly + Only type-check input program but do not verify it. + + -v, --verbose + Increase verbosity. Repeatable, but more than twice does not bring + more. + + --verbosity=LEVEL (absent=warning) + Be more or less verbose. LEVEL must be one of quiet, error, + warning, info or debug. Takes over -v. + +COMMON OPTIONS + --help[=FMT] (default=auto) + Show this help in format FMT. The value FMT must be one of auto, + pager, groff or plain. With auto, the format is pager or plain + whenever the TERM env var is dumb or undefined. + + --version + Show version information. +``` \ No newline at end of file diff --git a/lib/config/config.ml b/lib/config/config.ml index 79cffce..1c69105 100644 --- a/lib/config/config.ml +++ b/lib/config/config.ml @@ -1,7 +1,7 @@ (** Configuration and command line options *) (** Version string *) -let version = "0.1" +let version = "1.0" (** The command line options *) let cmd_options_spec = [] diff --git a/test/comparison/arc_atomics.rav b/test/comparison/arc_atomics.rav index fc5a59f..19a9ab1 100644 --- a/test/comparison/arc_atomics.rav +++ b/test/comparison/arc_atomics.rav @@ -3,7 +3,7 @@ include "arc_ra.rav" interface ARC[SharePred: ShareablePredicate] { field c: Int - field v: ArcRA + ghost field v: ArcRA // module SharePred: ShareablePredicate @@ -267,6 +267,6 @@ interface ARC[SharePred: ShareablePredicate] { commitAU(phi, v); fold arcInv(x); - return 1; + return v; } } diff --git a/test/comparison/inc_dec.rav b/test/comparison/inc_dec.rav index cf2ed33..686e5ca 100644 --- a/test/comparison/inc_dec.rav +++ b/test/comparison/inc_dec.rav @@ -8,7 +8,7 @@ proc incr(x: Ref, k: Int, implicit ghost v: Int) atomic requires counter(x, v) atomic ensures counter(x, v + k) { - var phi: AtomicToken := bindAU(); + ghost var phi: AtomicToken := bindAU(); ghost var v0: Int := openAU(phi); unfold counter(x, v0); @@ -33,7 +33,7 @@ proc incr(x: Ref, k: Int, implicit ghost v: Int) !} if (!res) { - var v3: Int := openAU(phi); + ghost var v3: Int := openAU(phi); incr(x, k); commitAU(phi); } @@ -43,7 +43,7 @@ proc decr(x: Ref, k: Int, implicit ghost v: Int) atomic requires counter(x, v) atomic ensures counter(x, v - k) { - var phi: AtomicToken := bindAU(); + ghost var phi: AtomicToken := bindAU(); ghost var v0: Int := openAU(phi); unfold counter(x, v0); @@ -68,7 +68,7 @@ proc decr(x: Ref, k: Int, implicit ghost v: Int) !} if (!res) { - var v3: Int := openAU(phi); + ghost var v3: Int := openAU(phi); decr(x, k); commitAU(phi); } @@ -79,7 +79,7 @@ proc read(x: Ref, implicit ghost v: Int) atomic requires counter(x, v) atomic ensures counter(x, v) && v2 == v { - var phi: AtomicToken := bindAU(); + ghost var phi: AtomicToken := bindAU(); ghost var v0: Int := openAU(phi); unfold counter(x, v0); diff --git a/test/comparison/lclist.rav b/test/comparison/lclist_wip.rav similarity index 100% rename from test/comparison/lclist.rav rename to test/comparison/lclist_wip.rav diff --git a/test/comparison/peterson.rav b/test/comparison/peterson.rav index 29530ca..c00ab6f 100644 --- a/test/comparison/peterson.rav +++ b/test/comparison/peterson.rav @@ -82,17 +82,17 @@ module Peterson[R: LockResource] ghost var or_l0: Bool; ghost var or_r0: Bool; ghost var or_tl0: Bool; ghost var or_tr0: Bool; - unfold peterson_inv(l, r){ - wl0 :| wl, - wr0 :| wr, - t0 :| t, - la0 :| la, - ra0 :| ra, - or_l0 :| or_l, - or_r0 :| or_r, - or_tl0 :| or_tl, - or_tr0 :| or_tr - }; + unfold peterson_inv(l, r)[ + wl0 := wl, + wr0 := wr, + t0 := t, + la0 := la, + ra0 := ra, + or_l0 := or_l, + or_r0 := or_r, + or_tl0 := or_tl, + or_tr0 := or_tr + ]; var wr : Bool := l.wait_right; @@ -131,17 +131,17 @@ module Peterson[R: LockResource] ghost var or_l1: Bool; ghost var or_r1: Bool; ghost var or_tl1: Bool; ghost var or_tr1: Bool; - unfold peterson_inv(l, r){ - wl1 :| wl, - wr1 :| wr, - t1 :| t, - la1 :| la, - ra1 :| ra, - or_l1 :| or_l, - or_r1 :| or_r, - or_tl1 :| or_tl, - or_tr1 :| or_tr - }; + unfold peterson_inv(l, r)[ + wl1 := wl, + wr1 := wr, + t1 := t, + la1 := la, + ra1 := ra, + or_l1 := or_l, + or_r1 := or_r, + or_tl1 := or_tl, + or_tr1 := or_tr + ]; var curr_turn : Bool := l.turn; assert own(l.active_left, true, 1.0); @@ -194,13 +194,13 @@ module Peterson[R: LockResource] ghost var or_l0: Bool; ghost var or_r0: Bool; ghost var or_tl0: Bool; ghost var or_tr0: Bool; - unfold peterson_inv(l, r){ - wl0 :| wl, - or_l0 :| or_l, - or_r0 :| or_r, - or_tl0 :| or_tl, - or_tr0 :| or_tr - }; + unfold peterson_inv(l, r)[ + wl0 := wl, + or_l0 := or_l, + or_r0 := or_r, + or_tl0 := or_tl, + or_tr0 := or_tr + ]; l.wait_left := true; fold peterson_inv(l, r)[ @@ -216,14 +216,14 @@ module Peterson[R: LockResource] ghost var or_l1: Bool; ghost var or_r1: Bool; ghost var or_tl1: Bool; ghost var or_tr1: Bool; - unfold peterson_inv(l, r){ - t1 :| t, - la1 :| la, - or_l1 :| or_l, - or_r1 :| or_r, - or_tl1 :| or_tl, - or_tr1 :| or_tr - }; + unfold peterson_inv(l, r)[ + t1 := t, + la1 := la, + or_l1 := or_l, + or_r1 := or_r, + or_tl1 := or_tl, + or_tr1 := or_tr + ]; // pass the turn to right l.turn := false; @@ -252,17 +252,17 @@ module Peterson[R: LockResource] ghost var or_l0: Bool; ghost var or_r0: Bool; ghost var or_tl0: Bool; ghost var or_tr0: Bool; - unfold peterson_inv(l, r){ - wl0 :| wl, - wr0 :| wr, - t0 :| t, - la0 :| la, - ra0 :| ra, - or_l0 :| or_l, - or_r0 :| or_r, - or_tl0 :| or_tl, - or_tr0 :| or_tr - }; + unfold peterson_inv(l, r)[ + wl0 := wl, + wr0 := wr, + t0 := t, + la0 := la, + ra0 := ra, + or_l0 := or_l, + or_r0 := or_r, + or_tl0 := or_tl, + or_tr0 := or_tr + ]; l.wait_left := false; {! @@ -295,17 +295,17 @@ module Peterson[R: LockResource] ghost var or_l0: Bool; ghost var or_r0: Bool; ghost var or_tl0: Bool; ghost var or_tr0: Bool; - unfold peterson_inv(l, r){ - wl0 :| wl, - wr0 :| wr, - t0 :| t, - la0 :| la, - ra0 :| ra, - or_l0 :| or_l, - or_r0 :| or_r, - or_tl0 :| or_tl, - or_tr0 :| or_tr - }; + unfold peterson_inv(l, r)[ + wl0 := wl, + wr0 := wr, + t0 := t, + la0 := la, + ra0 := ra, + or_l0 := or_l, + or_r0 := or_r, + or_tl0 := or_tl, + or_tr0 := or_tr + ]; var wl : Bool := l.wait_left; @@ -344,17 +344,17 @@ module Peterson[R: LockResource] ghost var or_l1: Bool; ghost var or_r1: Bool; ghost var or_tl1: Bool; ghost var or_tr1: Bool; - unfold peterson_inv(l, r){ - wl1 :| wl, - wr1 :| wr, - t1 :| t, - la1 :| la, - ra1 :| ra, - or_l1 :| or_l, - or_r1 :| or_r, - or_tl1 :| or_tl, - or_tr1 :| or_tr - }; + unfold peterson_inv(l, r)[ + wl1 := wl, + wr1 := wr, + t1 := t, + la1 := la, + ra1 := ra, + or_l1 := or_l, + or_r1 := or_r, + or_tl1 := or_tl, + or_tr1 := or_tr + ]; var curr_turn : Bool := l.turn; assert own(l.active_right, true, 1.0); @@ -406,13 +406,13 @@ module Peterson[R: LockResource] ghost var or_l0: Bool; ghost var or_r0: Bool; ghost var or_tl0: Bool; ghost var or_tr0: Bool; - unfold peterson_inv(l, r){ - wr0 :| wr, - or_l0 :| or_l, - or_r0 :| or_r, - or_tl0 :| or_tl, - or_tr0 :| or_tr - }; + unfold peterson_inv(l, r)[ + wr0 := wr, + or_l0 := or_l, + or_r0 := or_r, + or_tl0 := or_tl, + or_tr0 := or_tr + ]; l.wait_right := true; fold peterson_inv(l, r)[ @@ -428,14 +428,14 @@ module Peterson[R: LockResource] ghost var or_l1: Bool; ghost var or_r1: Bool; ghost var or_tl1: Bool; ghost var or_tr1: Bool; - unfold peterson_inv(l, r){ - t1 :| t, - ra1 :| ra, - or_l1 :| or_l, - or_r1 :| or_r, - or_tl1 :| or_tl, - or_tr1 :| or_tr - }; + unfold peterson_inv(l, r)[ + t1 := t, + ra1 := ra, + or_l1 := or_l, + or_r1 := or_r, + or_tl1 := or_tl, + or_tr1 := or_tr + ]; // pass the turn to left l.turn := true; @@ -464,17 +464,17 @@ module Peterson[R: LockResource] ghost var or_l0: Bool; ghost var or_r0: Bool; ghost var or_tl0: Bool; ghost var or_tr0: Bool; - unfold peterson_inv(l, r){ - wl0 :| wl, - wr0 :| wr, - t0 :| t, - la0 :| la, - ra0 :| ra, - or_l0 :| or_l, - or_r0 :| or_r, - or_tl0 :| or_tl, - or_tr0 :| or_tr - }; + unfold peterson_inv(l, r)[ + wl0 := wl, + wr0 := wr, + t0 := t, + la0 := la, + ra0 := ra, + or_l0 := or_l, + or_r0 := or_r, + or_tl0 := or_tl, + or_tr0 := or_tr + ]; l.wait_right := false; {! diff --git a/test/concurrent/lock/spin-lock_compact.rav b/test/concurrent/lock/spin-lock_compact.rav new file mode 100644 index 0000000..5b4c5fd --- /dev/null +++ b/test/concurrent/lock/spin-lock_compact.rav @@ -0,0 +1,65 @@ +include "lock.rav" + +module SpinLock[R: LockResource] { + field bit: Bool + + import R.resource + + module Agree = Library.Agree[R] + ghost field agr: Agree + + pred is_lock(l: Ref; r: R, b: Bool) { + own(l, agr, Agree.agree(r)) + && own(l, bit, b, 1.0) + && (b ? true : resource(r)) + } + + proc create(r: R) + returns (l: Ref) + requires resource(r) + ensures is_lock(l, r, false) + { + l := new (bit: false, agr: Agree.agree(r)); + fold is_lock(l, r, false); + } + + proc acquire(l: Ref, implicit ghost r: R, implicit ghost b: Bool) + atomic requires is_lock(l, r, b) + atomic ensures is_lock(l, r, true) && b == false && resource(r) + { + ghost val phi: AtomicToken = bindAU(); + + ghost var b1: Bool; + r, b1 := openAU(phi); unfold is_lock(l, r, b1); + + val res: Bool := cas(l.bit, false, true); + {! + fold is_lock(l, r, true); + if (res) { + commitAU(phi); + } else { + abortAU(phi); + } + !} + + if (res) { + return; + } + + r, b1 := openAU(phi); + acquire(l, r, b1); + commitAU(phi); + } + + proc release(l: Ref, implicit ghost r: R) + atomic requires is_lock(l, r, true) && resource(r) + atomic ensures is_lock(l, r, false) + { + ghost val phi: AtomicToken = bindAU(); + r := openAU(phi); + unfold is_lock(l, r, true); + l.bit := false; + fold is_lock(l, r, false); + commitAU(phi); + } +} diff --git a/test/concurrent/lock/ticket-lock_program_no-proof.rav b/test/concurrent/lock/ticket-lock_program_failing_no-proof.rav similarity index 100% rename from test/concurrent/lock/ticket-lock_program_no-proof.rav rename to test/concurrent/lock/ticket-lock_program_failing_no-proof.rav diff --git a/test/concurrent/templates/give-up-lock.rav b/test/concurrent/templates/give-up-lock.rav deleted file mode 100644 index 75114ff..0000000 --- a/test/concurrent/templates/give-up-lock.rav +++ /dev/null @@ -1,665 +0,0 @@ -include "./flows_ra.rav" -include "./ccm_instances.rav" -include "./keyset_ra.rav" -include "../lock/lock.rav" - -import Library.Type -import Library.CancellativeResourceAlgebra - -interface Keyspace { - rep type T - - val ks: Set[T] -} - -module IntKeyspace : Keyspace { - rep type T = Int - - val ks: Set[T] = {| k: Int :: true |} -} - -interface SearchStructureSpec { - type K - val keyspace: Set[K] - - type Op = data { case searchOp ; case insertOp ; case deleteOp } - - pred opSpec(op: Op, k: K, c_in: Set[K], c_out: Set[K], res: Bool) { - op == searchOp() ? - c_in == c_out && res == (k in c_in) : - (op == insertOp() ? - c_out == c_in ++ {| k |} && res == (k !in c_in) : - c_out == c_in -- {| k |} && res == (k in c_in)) - } -} - -interface Node { - rep type T -} - -interface NodeImpl { - - module Spec : SearchStructureSpec - import Spec._ - - module K_Type : Library.Type { - rep type T = K - } - - module Multiset_K = Multiset[K_Type] - module Flow_K = FlowsRA[Multiset_K] - - import Flow_K._ - import Multiset_K.elem - - pred node(n: Ref; c: Set[K], i: Flow_K) - - // func outsets(outset: Map[Ref, Set[K]]) returns (ret: Set[K]) - // { - // {| k: K :: exists r: Ref :: k in outset[r] |} - // } - - // func keyset(inset: Set[K], outset: Map[Ref, Set[K]]) returns (ret: Set[K]) - // { - // inset -- outsets(outset) - // } - - func inset(i: Flow_K.T, n: Ref) returns (ret: Set[K]) - { - {| k : K :: (i.inf[n])[k] > 0 |} - } - - func insets(i: Flow_K.T) returns (ret: Set[K]) - { - {| k : K :: exists n: Ref :: n in i.dom && k in inset(i, n) |} - } - - func outset(i: Flow_K.T, n: Ref) returns (ret: Set[K]) - { - {| k : K :: (i.out[n])[k] > 0 |} - } - - func outsets(i: Flow_K.T) returns (ret: Set[K]) - { - {| k: K :: exists n: Ref :: n !in i.dom && k in outset(i,n) |} - } - - func keyset(i: Flow_K.T) returns (ret: Set[K]) - { - insets(i) -- outsets(i) - } - - proc createRoot() - returns (r: Ref) - ensures node(r, {||}, - Flow_K.int({| l:Ref :: l == r ? Multiset_K.fromSet(keyspace) : Multiset_K.id |}, zeroFlow, {| r |})) - - proc decisiveOp(dop: Op, n: Ref, k: K, implicit ghost c: Set[K], implicit ghost i_n: Flow_K) - returns (succ: Bool, res: Bool, implicit ghost c1: Set[K]) - requires k in keyset(i_n) - requires node(n, c, i_n) - ensures node(n, c1, i_n) - ensures succ ==> opSpec(dop, k, c, c1, res) - ensures !succ ==> c == c1 - - proc findNext(n: Ref, k: K, implicit ghost c: Set[K], implicit ghost i_n: Flow_K) - returns (ret: Bool, n1: Ref) - requires k in inset(i_n, n) - requires node(n, c, i_n) - ensures node(n, c, i_n) && - (ret ? - k in outset(i_n, n1) : - k !in outsets(i_n)) - - proc inRange(n: Ref, k: K, implicit ghost c: Set[K], implicit ghost i_n: Flow_K) - returns (ret: Bool) - requires node(n, c, i_n) - ensures node(n, c, i_n) && (ret ==> k in inset(i_n, n)) - - - lemma nodeSepStar(n: Ref, c1: Set[K], c2: Set[K], i_n1: Flow_K, i_n2: Flow_K) - requires node(n, c1, i_n1) && node(n, c2, i_n2) - ensures false -} - -// interface SearchStructure { -// module Spec: SearchStructureSpec -// import Spec._ - -// pred css(r: Ref, c: Set[K]) - -// // inv cssInv(r: Ref) - -// proc create() -// returns (r: Ref) -// ensures css(r, {||}) - -// // proc cssOp(dop: Op, r: Ref, k: K, implicit ghost c: Set[K]) -// // returns (res: Bool, implicit ghost c1: Set[K]) -// // requires k in keyset -// // // requires cssInv(r) -// // atomic requires cssR(r, c) -// // atomic ensures cssR(r, c1) && opSpec(dop, k, c, c1, res) -// } - - -interface GiveUpTemplate[Node: NodeImpl, LockF: Lock] { - module Spec: SearchStructureSpec = Node.Spec - import Node.Spec._ - import Node._ - import Node.Flow_K._ - import Node.Multiset_K.elem - import Node.Multiset_K.fromSet - - module Ref_Type : Library.Type { - rep type T = Ref - } - - module SetRefRA = Library.SetRA[Ref_Type] - - module AuthSetRef = Library.Auth[SetRefRA] - - module Keyset_K = KeysetRA[K_Type] - module AuthKeyset_K = Library.Auth[Keyset_K] - module AuthFlow_K = Library.Auth[Flow_K] - - field authSet: AuthSetRef - field authKS: AuthKeyset_K - field authFlow: AuthFlow_K - field lock: Ref - - module N : LockResource { - rep type T = (Ref, Ref) - - pred resource(r: T) { - exists c: Set[K], i_n: Flow_K :: - nodePred(r#0, r#1, c, i_n) - } - - pred nodePred(r: Ref, n: Ref; c: Set[K], i_n: Flow_K) { - own(r.authKS, AuthKeyset_K.frag( Keyset_K.prodKS( keyset(i_n), c ) )) && - own(r.authFlow, AuthFlow_K.frag(i_n)) && - i_n.dom == {|n|} && - Node.node(n, c, i_n) - } - } - - module L = LockF[N] - - pred globalinv(g_i: Flow_K, r: Ref) { - Flow_K.valid(g_i) && - r in g_i.dom && - outsets(g_i) == {||} && - inset(g_i, r) == keyspace - } - - pred globalRes(r: Ref, c: Set[K], g_i: Flow_K) { - own(r.authKS, AuthKeyset_K.auth( Keyset_K.prodKS( keyspace, c ))) && - own(r.authSet, AuthSetRef.auth(SetRefRA.set_constr(g_i.dom))) && - own(r.authFlow, AuthFlow_K.auth(g_i)) && - globalinv(g_i, r) - } - - /*pred nodePred(r: Ref, n: Ref; c: Set[K], i_n: Flow_K) { - own(r.authKS, AuthKeyset_K.frag( Keyset_K.prodKS( keyset(i_n), c ) )) && - own(r.authFlow, AuthFlow_K.frag(i_n)) && - i_n.dom == {|n|} && - Node.node(n, c, i_n) - }*/ - - pred inFP(r: Ref, n: Ref) { - own(r.authSet, AuthSetRef.frag(SetRefRA.set_constr({|n|})) ) - } - - pred cssR(r: Ref, c: Set[K], g_i: Flow_K, lockval: Map[Ref, Int]) { - (forall n: Ref :: n in g_i.dom ==> - (exists l: Ref :: - L.is_lock(l, (r, n), lockval[n] == 1) && own(n.lock, l, 1.0))) - && - globalRes(r, c, g_i) - } - - pred css(r: Ref, c: Set[K]) { - exists g_i: Flow_K, lockval: Map[Ref, Int] :: - cssR(r, c, g_i, lockval) - } - - lemma cssInFp(r: Ref, n:Ref, c: Set[K], g_i: Flow_K, lockval: Map[Ref, Int]) - requires cssR(r, c, g_i, lockval) - requires inFP(r, n) - ensures n in g_i.dom - ensures cssR(r, c, g_i, lockval) - ensures inFP(r, n) - { - unfold cssR(r, c, g_i, lockval); - unfold globalRes(r, c, g_i); - unfold inFP(r, n); - - fold globalRes(r, c, g_i); - fold inFP(r, n); - fold cssR(r, c, g_i, lockval); - } - - - lemma fpInCss(r: Ref, n:Ref, c: Set[K], g_i: Flow_K, lockval: Map[Ref, Int]) - requires cssR(r, c, g_i, lockval) - requires n in g_i.dom - ensures inFP(r, n) - ensures cssR(r, c, g_i, lockval) - { - unfold cssR(r, c, g_i, lockval); - unfold globalRes(r, c, g_i); - - fpu(r, authSet, AuthSetRef.auth(SetRefRA.set_constr(g_i.dom)), AuthSetRef.auth_frag(SetRefRA.set_constr(g_i.dom), SetRefRA.set_constr(g_i.dom))); - - fold globalRes(r, c, g_i); - fold inFP(r, n); - fold cssR(r, c, g_i, lockval); - } - - lemma root_fp(r: Ref, c: Set[K], g_i: Flow_K, lockval: Map[Ref, Int]) - requires cssR(r, c, g_i, lockval) - ensures cssR(r, c, g_i, lockval) - ensures r in g_i.dom - { - unfold cssR(r, c, g_i, lockval); - unfold globalRes(r, c, g_i); - unfold globalinv(g_i, r); - - fold globalinv(g_i, r); - fold globalRes(r, c, g_i); - fold cssR(r, c, g_i, lockval); - } - - // proc lockNode(n: Ref, implicit ghost b: Int) - // atomic requires own(n.lock, b, 1.0) - // atomic ensures own(n.lock, 1, 1.0) && b == 0 - - // proc unlockNode(n: Ref) - // atomic requires own(n.lock, 1, 1.0) - // atomic ensures own(n.lock, 0, 1.0) - -/* - proc lockNodeHigh(r: Ref, n: Ref, implicit ghost c: Set[K]) - returns (ghost c_n : Set[K], ghost i_n: Flow_K) - requires inFP(r, n) - atomic requires css(r, c) - atomic ensures css(r, c) && N.nodePred(r, n, c_n, i_n) && inFP(r, n) - { - var phi: AtomicToken := bindAU(); - - ghost var g_i0: Flow_K; - ghost var lockval0: Map[Ref, Int]; - - ghost val c0: Set[K] := openAU(phi); - unfold css(r, c0); - g_i0, lockval0 :| cssR(r, c0, g_i0, lockval0); - cssInFp(r, n, c0, g_i0, lockval0); - - unfold cssR(r, c0, g_i0, lockval0); - - L.acquire(n.lock); - unfold N.resource((r, n)); - ghost var c_n1 : Set[K]; ghost var i_n1: Flow_K; - c_n1, i_n1 :| N.nodePred(r, n, c_n1, i_n1); - ghost var lockval00: Map[Ref, Int] := lockval0[n := 1]; - fold cssR(r, c0, g_i0, lockval00); - assert cssR(r, c0, g_i0, lockval00); - fold css(r, c0); - - commitAU(phi, c_n1, i_n1); - return c_n1, i_n1; - } - - proc unlockNodeHigh(r: Ref, n: Ref, implicit ghost c_n: Set[K], implicit ghost i_n: Flow_K, implicit ghost c: Set[K]) - requires inFP(r, n) - requires N.nodePred(r, n, c_n, i_n) - atomic requires css(r, c) - atomic ensures css(r, c) && inFP(r, n) - { - ghost var phi: AtomicToken := bindAU(); - - ghost var g_i1: Flow_K; - ghost var lockval1: Map[Ref, Int]; - - ghost var c1: Set[K]; - c_n, i_n, c1 := openAU(phi); - unfold css(r, c1); - g_i1, lockval1 :| cssR(r, c1, g_i1, lockval1); - cssInFp(r, n, c1, g_i1, lockval1); - - unfold cssR(r, c1, g_i1, lockval1); - - {! - if (lockval1[n] != 1) { - L.exclusive(n.lock, (r,n)); - } - !} - - L.release(n.lock); - ghost var lockval2: Map[Ref, Int] := lockval1[n := 0]; - //ghost var contents2: Map[Ref, Set[K]] := contents1[n := c_n]; - //ghost var intf2: Map[Ref, Flow_K] := intf1[n := i_n]; - - fold cssR(r, c1, g_i1, lockval2); - assert cssR(r, c1, g_i1, lockval2); - fold css(r, c1); - - commitAU(phi); - } - - proc create() - returns (r: Ref) - ensures css(r, {||}) - { - r := Node.createRoot(); - - var i_r: Flow_K := int( - {| l:Ref :: l == r ? fromSet(keyspace) : fromSet({||}) |}, - zeroFlow(), - {|r|} - ); - var contents: Map[Ref, Set[K]] := {| l: Ref :: {||} |}; - var lockval: Map[Ref, Int] := {| l: Ref :: 0 |}; - var intf: Map[Ref, Flow_K] := {| l: Ref :: l == r ? i_r : Flow_K.id |}; - - r := new( - authKS: AuthKeyset_K.auth_frag( - Keyset_K.prodKS(keyspace, {||}), - Keyset_K.prodKS(keyspace, {||}) - ), - authSet:AuthSetRef.auth(SetRefRA.set_constr({|r|})), - authFlow: AuthFlow_K.auth_frag( - i_r, i_r - ), - lock:0 - ); - - fold N.resource((r, r, {||}, i_r)); - - fold globalinv(i_r, r); - fold globalRes(r, {||}, i_r); - fold cssR(r, {||}, i_r, lockval, contents, intf); - assert cssR(r, {||}, i_r, lockval, contents, intf); - fold css(r, {||}); - } - - lemma fpInStep(r: Ref, n: Ref, n1: Ref, k: K, c: Set[K], g_i: Flow_K, lockval: Map[Ref, Int], contents: Map[Ref, Set[K]], intf: Map[Ref, Flow_K], c_n: Set[K], i_n: Flow_K) - requires cssR(r, c, g_i, lockval, contents, intf) - requires N.resource((r, n, c_n, i_n)) - requires k in outset(i_n, n1) - requires n in g_i.dom - ensures cssR(r, c, g_i, lockval, contents, intf) - ensures N.resource((r, n, c_n, i_n)) - ensures n1 in g_i.dom - { - if (n1 !in g_i.dom) { - unfold cssR(r, c, g_i, lockval, contents, intf); - unfold N.resource((r, n, c_n, i_n)); - - unfold globalRes(r, c, g_i); - unfold globalinv(g_i, r); - - ghost var i_o: Flow_K = Flow_K.frame(g_i, i_n); - // assert Flow_K.valid(i_o); - - assert k !in outsets(g_i); - - fold N.resource((r, n, c_n, i_n)); - fold globalinv(g_i, r); - fold globalRes(r, c, g_i); - fold cssR(r, c, g_i, lockval, contents, intf); - } - } - - proc traverse(r: Ref, n: Ref, k: K, implicit ghost c: Set[K]) - returns (nn: Ref, cnn: Set[K], i_nn: Flow_K) - requires inFP(r, n) - atomic requires css(r, c) - atomic ensures css(r, c) - ensures N.resource((r, nn, cnn, i_nn)) - ensures inFP(r, nn) - ensures k in keyset(i_nn) - { - ghost val phi: AtomicToken := bindAU(); - - ghost var c_n: Set[K]; - ghost var i_n: Flow_K; - - ghost val c0: Set[K] := openAU(phi); - c_n, i_n := lockNodeHigh(r, n, c0); - abortAU(phi); - - unfold N.resource((r, n, c_n, i_n)); - - var in_range: Bool := Node.inRange(n, k, c_n, i_n); - - if (in_range) { - var succ: Bool; - var n1: Ref; - succ, n1 := Node.findNext(n, k, c_n, i_n); - - fold N.resource((r, n, c_n, i_n)); - - if (succ) { - ghost var g_i1: Flow_K; - ghost var lockval1: Map[Ref, Int]; - ghost var contents1: Map[Ref, Set[K]]; - ghost var intf1: Map[Ref, Flow_K]; - - ghost val c1: Set[K] := openAU(phi); - unfold css(r, c1); - g_i1, lockval1, contents1, intf1 :| cssR(r, c1, g_i1, lockval1, contents1, intf1); - - cssInFp(r, n, c1, g_i1, lockval1, contents1, intf1); - fpInStep(r, n, n1, k, c1, g_i1, lockval1, contents1, intf1, c_n, i_n); - fpInCss(r, n1, c1, g_i1, lockval1, contents1, intf1); - - assert cssR(r, c1, g_i1, lockval1, contents1, intf1); - fold css(r, c1); - - unlockNodeHigh(r, n, c_n, i_n, c1); - - abortAU(phi); - - ghost val c2: Set[K] := openAU(phi); - - nn, cnn, i_nn := traverse(r, n1, k, c2); - - commitAU(phi, nn, cnn, i_nn); - return nn, cnn, i_nn; - } else { - ghost val c0: Set[K] := openAU(phi); - unlockNodeHigh(r, n, c_n, i_n, c0); - abortAU(phi); - - ghost var g_i1: Flow_K; - ghost var lockval1: Map[Ref, Int]; - ghost var contents1: Map[Ref, Set[K]]; - ghost var intf1: Map[Ref, Flow_K]; - - ghost val c1: Set[K] := openAU(phi); - - commitAU(phi, n, c_n, i_n); - return n, c_n, i_n; - } - } else { - - fold nodePred(r, n, c_n, i_n); - - ghost val c0: Set[K] := openAU(phi); - unlockNodeHigh(r, n, c_n, i_n, c0); - abortAU(phi); - - ghost var g_i1: Flow_K; - ghost var lockval1: Map[Ref, Int]; - ghost var contents1: Map[Ref, Set[K]]; - ghost var intf1: Map[Ref, Flow_K]; - - ghost val c1: Set[K] := openAU(phi); - - unfold css(r, c1); - g_i1, lockval1, contents1, intf1 :| cssR(r, c1, g_i1, lockval1, contents1, intf1); - - unfold cssR(r, c1, g_i1, lockval1, contents1, intf1); - unfold globalRes(r, c1, g_i1); - unfold globalinv(g_i1, r); - - fold globalinv(g_i1, r); - fold globalRes(r, c1, g_i1); - fold cssR(r, c1, g_i1, lockval1, contents1, intf1); - - fpInCss(r, r, c1, g_i1, lockval1, contents1, intf1); - - assert cssR(r, c1, g_i1, lockval1, contents1, intf1); - fold css(r, c1); - nn, cnn, i_nn := traverse(r, r, k, c1); - - commitAU(phi, nn, cnn, i_nn); - } - } - - lemma keyset_theorem(r: Ref, dop: Op, k: K, c_n: Set[K], c_n1: Set[K], c: Set[K], res: Bool, k_n: Set[K]) - returns (c1: Set[K]) - requires opSpec(dop, k, c_n, c_n1, res) - requires own(r.authKS, AuthKeyset_K.auth(Keyset_K.prodKS(keyspace, c))) - requires own(r.authKS, AuthKeyset_K.frag(Keyset_K.prodKS(k_n, c_n))) - // requires own(r.authFlow, AuthFlow_K.auth(g_i))requires own(r.authFlow, AuthFlow_K.frag(g_i)) - requires c_n1 subseteq k_n - requires k in k_n - requires k in keyspace - - ensures opSpec(dop, k, c, c1, res) - ensures own(r.authKS, AuthKeyset_K.auth(Keyset_K.prodKS(keyspace, c1))) - ensures own(r.authKS, AuthKeyset_K.frag(Keyset_K.prodKS(k_n, c_n1))) - { - unfold opSpec(dop, k, c_n, c_n1, res); - - if (dop == searchOp() || !res) { - c1 := c; - fold opSpec(dop, k, c, c1, res); - } else { - if (dop == insertOp()) { - c1 := c ++ {| k |}; - } else { - c1 := c -- {| k |}; - } - - {! - fold opSpec(dop, k, c, c1, res); - - /*assert AuthKeyset_K.fpuAllowed( - AuthKeyset_K.auth_frag(Keyset_K.prodKS(keyspace, c), Keyset_K.prodKS(k_n, c_n)), - AuthKeyset_K.auth_frag(Keyset_K.prodKS(keyspace, c1), Keyset_K.prodKS(k_n, c_n1)) - ) with { - assert forall k: Keyset_K :: {Keyset_K.comp(k, Keyset_K.prodKS(k_n, c_n1))} {Keyset_K.comp(k, Keyset_K.prodKS(k_n, c_n))} - Keyset_K.prodKS(keyspace, c) == Keyset_K.comp(k, Keyset_K.prodKS(k_n, c_n)) ==> - Keyset_K.prodKS(keyspace, c1) == Keyset_K.comp(k, Keyset_K.prodKS(k_n, c_n1)); - - //assert AuthKeyset_K.valid(AuthKeyset_K.auth_frag(Keyset_K.prodKS(keyspace, c), Keyset_K.prodKS(k_n, c_n))); - //assert AuthKeyset_K.valid(AuthKeyset_K.auth_frag(Keyset_K.prodKS(keyspace, c1), Keyset_K.prodKS(k_n, c_n1))); - }*/ - - fpu(r, authKS, - AuthKeyset_K.auth_frag(Keyset_K.prodKS(keyspace, c), Keyset_K.prodKS(k_n, c_n)), - AuthKeyset_K.auth_frag(Keyset_K.prodKS(keyspace, c1), Keyset_K.prodKS(k_n, c_n1))); - !} - } - } - - proc cssOp(dop: Op, r: Ref, k: K, implicit ghost c: Set[K]) - returns (res: Bool, implicit ghost cc: Set[K]) - requires k in keyspace - atomic requires css(r, c) - atomic ensures css(r, cc) && opSpec(dop, k, c, cc, res) - { - ghost val phi: AtomicToken := bindAU(); - - var n: Ref; - var c_n: Set[K]; - var i_n: Flow_K; - ghost var g_i0: Flow_K; - ghost var lockval0: Map[Ref, Int]; - ghost var contents0: Map[Ref, Set[K]]; - ghost var intf0: Map[Ref, Flow_K]; - - ghost val c0: Set[K] := openAU(phi); - unfold css(r, c0); - g_i0, lockval0, contents0, intf0 :| cssR(r, c0, g_i0, lockval0, contents0, intf0); - - root_fp(r, c0, g_i0, lockval0, contents0, intf0); - fpInCss(r, r, c0, g_i0, lockval0, contents0, intf0); - assert cssR(r, c0, g_i0, lockval0, contents0, intf0); - fold css(r, c0); - - n, c_n, i_n := traverse(r, r, k, c0); - - abortAU(phi); - - var succ: Bool; - var c_n1: Set[K]; - - unfold N.resource((r, n, c_n, i_n)); - //assert own(r.authFlow, AuthFlow_K.frag(i_n)); - - succ, res, c_n1 := Node.decisiveOp(dop, n, k, c_n, i_n); - if (succ) { - - ghost var g_i1: Flow_K; - ghost var lockval1: Map[Ref, Int]; - ghost var contents1: Map[Ref, Set[K]]; - ghost var intf1: Map[Ref, Flow_K]; - - ghost val c1: Set[K] := openAU(phi); - unfold css(r, c1); - g_i1, lockval1, contents1, intf1 :| cssR(r, c1, g_i1, lockval1, contents1, intf1); - cssInFp(r, n, c1, g_i1, lockval1, contents1, intf1); - unfold cssR(r, c1, g_i1, lockval1, contents1, intf1); - - {! - if (lockval1[n] != 1) { - unfold N.resource((r, n, contents1[n], intf1[n])); - Node.nodeSepStar(n, c_n1, contents1[n], i_n, intf1[n]); - } - !} - - unlockNode(n); - - unfold globalRes(r, c1, g_i1); - unfold opSpec(dop, k, c_n, c_n1, res); - fold opSpec(dop, k, c_n, c_n1, res); - - cc := keyset_theorem(r, dop, k, c_n, c_n1, c1, res, keyset(i_n)); - - /*AuthFlow_K.compValid(); - AuthFlow_K.weak_frameCompInv();*/ - - fold globalRes(r, cc, g_i1); - ghost var lockval2: Map[Ref, Int] := lockval1[n := 0]; - ghost var contents2: Map[Ref, Set[K]] := contents1[n := c_n1]; - ghost var intf2: Map[Ref, Flow_K] := intf1[n := i_n]; - - //Flow_K.compFrameInv(); - //Flow_K.frameCompInv(); - fold nodePred(r, n, contents2[n], intf2[n]); - fold cssR(r, cc, g_i1, lockval2, contents2, intf2); - assert cssR(r, cc, g_i1, lockval2, contents2, intf2); - fold css(r, cc); - - commitAU(phi, res, cc); - - return res, cc; - } else { - fold nodePred(r, n, c_n, i_n); - ghost val c0: Set[K] := openAU(phi); - unlockNodeHigh(r, n, c_n, i_n, c0); - abortAU(phi); - - ghost val c1: Set[K] := openAU(phi); - res, cc := cssOp(dop, r, k, c1); - commitAU(phi, res, cc); - - return res, cc; - } - }*/ -} \ No newline at end of file diff --git a/test/concurrent/templates/give-up-lock_wip.rav b/test/concurrent/templates/give-up-lock_wip.rav new file mode 100644 index 0000000..652eeb7 --- /dev/null +++ b/test/concurrent/templates/give-up-lock_wip.rav @@ -0,0 +1,235 @@ +include "./flows_ra.rav" +include "./ccm_instances.rav" +include "./keyset_ra.rav" +include "../lock/lock.rav" + +import Library.Type +import Library.CancellativeResourceAlgebra + +interface Keyspace { + rep type T + + val ks: Set[T] +} + +module IntKeyspace : Keyspace { + rep type T = Int + + val ks: Set[T] = {| k: Int :: true |} +} + +interface SearchStructureSpec { + type K + val keyspace: Set[K] + + type Op = data { case searchOp ; case insertOp ; case deleteOp } + + pred opSpec(op: Op, k: K, c_in: Set[K], c_out: Set[K], res: Bool) { + op == searchOp() ? + c_in == c_out && res == (k in c_in) : + (op == insertOp() ? + c_out == c_in ++ {| k |} && res == (k !in c_in) : + c_out == c_in -- {| k |} && res == (k in c_in)) + } +} + +interface Node { + rep type T +} + +interface NodeImpl { + + module Spec : SearchStructureSpec + import Spec._ + + module K_Type : Library.Type { + rep type T = K + } + + module Multiset_K = Multiset[K_Type] + module Flow_K = FlowsRA[Multiset_K] + + import Flow_K._ + import Multiset_K.elem + + pred node(n: Ref; c: Set[K], i: Flow_K) + + func inset(i: Flow_K.T, n: Ref) returns (ret: Set[K]) + { + {| k : K :: (i.inf[n])[k] > 0 |} + } + + func insets(i: Flow_K.T) returns (ret: Set[K]) + { + {| k : K :: exists n: Ref :: n in i.dom && k in inset(i, n) |} + } + + func outset(i: Flow_K.T, n: Ref) returns (ret: Set[K]) + { + {| k : K :: (i.out[n])[k] > 0 |} + } + + func outsets(i: Flow_K.T) returns (ret: Set[K]) + { + {| k: K :: exists n: Ref :: n !in i.dom && k in outset(i,n) |} + } + + func keyset(i: Flow_K.T) returns (ret: Set[K]) + { + insets(i) -- outsets(i) + } + + proc createRoot() + returns (r: Ref) + ensures node(r, {||}, + Flow_K.int({| l:Ref :: l == r ? Multiset_K.fromSet(keyspace) : Multiset_K.id |}, zeroFlow, {| r |})) + + proc decisiveOp(dop: Op, n: Ref, k: K, implicit ghost c: Set[K], implicit ghost i_n: Flow_K) + returns (succ: Bool, res: Bool, implicit ghost c1: Set[K]) + requires k in keyset(i_n) + requires node(n, c, i_n) + ensures node(n, c1, i_n) + ensures succ ==> opSpec(dop, k, c, c1, res) + ensures !succ ==> c == c1 + + proc findNext(n: Ref, k: K, implicit ghost c: Set[K], implicit ghost i_n: Flow_K) + returns (ret: Bool, n1: Ref) + requires k in inset(i_n, n) + requires node(n, c, i_n) + ensures node(n, c, i_n) && + (ret ? + k in outset(i_n, n1) : + k !in outsets(i_n)) + + proc inRange(n: Ref, k: K, implicit ghost c: Set[K], implicit ghost i_n: Flow_K) + returns (ret: Bool) + requires node(n, c, i_n) + ensures node(n, c, i_n) && (ret ==> k in inset(i_n, n)) + + + lemma nodeSepStar(n: Ref, c1: Set[K], c2: Set[K], i_n1: Flow_K, i_n2: Flow_K) + requires node(n, c1, i_n1) && node(n, c2, i_n2) + ensures false +} + +interface GiveUpTemplate[Node: NodeImpl, LockF: Lock] { + module Spec: SearchStructureSpec = Node.Spec + import Node.Spec._ + import Node._ + import Node.Flow_K._ + import Node.Multiset_K.elem + import Node.Multiset_K.fromSet + + module Ref_Type : Library.Type { + rep type T = Ref + } + + module SetRefRA = Library.SetRA[Ref_Type] + + module AuthSetRef = Library.Auth[SetRefRA] + + module Keyset_K = KeysetRA[K_Type] + module AuthKeyset_K = Library.Auth[Keyset_K] + module AuthFlow_K = Library.Auth[Flow_K] + + ghost field authSet: AuthSetRef + ghost field authKS: AuthKeyset_K + ghost field authFlow: AuthFlow_K + ghost field lock: Ref + + module N : LockResource { + rep type T = (Ref, Ref) + + pred resource(r: T) { + exists c: Set[K], i_n: Flow_K :: + nodePred(r#0, r#1, c, i_n) + } + + pred nodePred(r: Ref, n: Ref; c: Set[K], i_n: Flow_K) { + own(r.authKS, AuthKeyset_K.frag( Keyset_K.prodKS( keyset(i_n), c ) )) && + own(r.authFlow, AuthFlow_K.frag(i_n)) && + i_n.dom == {|n|} && + Node.node(n, c, i_n) + } + } + + module L = LockF[N] + + pred globalinv(g_i: Flow_K, r: Ref) { + Flow_K.valid(g_i) && + r in g_i.dom && + outsets(g_i) == {||} && + inset(g_i, r) == keyspace + } + + pred globalRes(r: Ref, c: Set[K], g_i: Flow_K) { + own(r.authKS, AuthKeyset_K.auth( Keyset_K.prodKS( keyspace, c ))) && + own(r.authSet, AuthSetRef.auth(SetRefRA.set_constr(g_i.dom))) && + own(r.authFlow, AuthFlow_K.auth(g_i)) && + globalinv(g_i, r) + } + + pred inFP(r: Ref, n: Ref) { + own(r.authSet, AuthSetRef.frag(SetRefRA.set_constr({|n|})) ) + } + + pred cssR(r: Ref, c: Set[K], g_i: Flow_K, lockval: Map[Ref, Int]) { + (forall n: Ref :: n in g_i.dom ==> + (exists l: Ref :: + L.is_lock(l, (r, n), lockval[n] == 1) && own(n.lock, l, 1.0))) + && + globalRes(r, c, g_i) + } + + pred css(r: Ref, c: Set[K]) { + exists g_i: Flow_K, lockval: Map[Ref, Int] :: + cssR(r, c, g_i, lockval) + } + + lemma cssInFp(r: Ref, n:Ref, c: Set[K], g_i: Flow_K, lockval: Map[Ref, Int]) + requires cssR(r, c, g_i, lockval) + requires inFP(r, n) + ensures n in g_i.dom + ensures cssR(r, c, g_i, lockval) + ensures inFP(r, n) + { + unfold cssR(r, c, g_i, lockval); + unfold globalRes(r, c, g_i); + unfold inFP(r, n); + + fold globalRes(r, c, g_i); + fold inFP(r, n); + fold cssR(r, c, g_i, lockval); + } + + + lemma fpInCss(r: Ref, n:Ref, c: Set[K], g_i: Flow_K, lockval: Map[Ref, Int]) + requires cssR(r, c, g_i, lockval) + requires n in g_i.dom + ensures inFP(r, n) + ensures cssR(r, c, g_i, lockval) + { + unfold cssR(r, c, g_i, lockval); + unfold globalRes(r, c, g_i); + + fpu(r, authSet, AuthSetRef.auth(SetRefRA.set_constr(g_i.dom)), AuthSetRef.auth_frag(SetRefRA.set_constr(g_i.dom), SetRefRA.set_constr(g_i.dom))); + + fold globalRes(r, c, g_i); + fold inFP(r, n); + fold cssR(r, c, g_i, lockval); + } + + lemma root_fp(r: Ref, c: Set[K], g_i: Flow_K, lockval: Map[Ref, Int]) + requires cssR(r, c, g_i, lockval) + ensures cssR(r, c, g_i, lockval) + ensures r in g_i.dom + { + unfold cssR(r, c, g_i, lockval); + unfold globalRes(r, c, g_i); + unfold globalinv(g_i, r); + + fold globalinv(g_i, r); + fold globalRes(r, c, g_i); + fold cssR(r, c, g_i, lockval); + } +} \ No newline at end of file diff --git a/test/concurrent/templates/single-node-compact.rav b/test/concurrent/templates/single-node-compact.rav deleted file mode 100644 index 113c6f3..0000000 --- a/test/concurrent/templates/single-node-compact.rav +++ /dev/null @@ -1,245 +0,0 @@ -module Lock { - rep type T = Ref - - field bit: Bool - - pred lock(l: Ref, b: Bool) { - own(l.bit, b, 1.0) - } - - proc create() - returns (l: T) - ensures lock(l, false) - { - l := new(bit:false); - - {! - fold lock(l, false); - !} - } - - proc acquire(l: T, implicit ghost b: Bool) - requires lock(l, b) - ensures lock(l, true) // && b == false - { - {! - unfold lock(l, b); - !} - - var res: Bool; - - if (l.bit) { /* can use l.bit OR b*/ - res := false; - } - - else { - res := true; - l.bit := true; - } - - {! - if (res) { - fold lock(l, true); - assert (lock(l, true) && b == false); - } else { - fold lock(l, true); - assert(lock(l, b)); - } - !} - - if (!res) { - acquire(l, b); - } - } - - proc release(l: T) - requires lock(l, true) - ensures lock(l, false) - { - {! - unfold lock(l, true); - !} - - l.bit := false; - - {! - fold lock(l, false); - assert (lock(l, false)); - !} - } -} - - -interface Keyspace { - rep type T - val ks: Set[T] -} - -module SearchStructureSpec[K: Keyspace] { - - type Op = data { case searchOp; case insertOp; case deleteOp } - - pred opSpec(op: Op, k: K, c: Set[K], c1: Set[K], res: Bool) { - op == searchOp() ? - c1 == c && res == (k in c) : - (op == insertOp() ? - c1 == c ++ {|k|} && res == (k !in c) : - - // op == deleteOp - c1 == c -- {|k|} && res == (k in c) - ) - } -} - -interface NodeImpl[K: Keyspace] { - module Spec = SearchStructureSpec[K] - import Spec - - rep type T - - pred nodeR(n: T, c: Set[Spec.K]) - - proc create() - returns (n: T) - ensures nodeR(n, {||}) - - proc decisiveOp(dop: Spec.Op, n: T, k: Spec.K, implicit ghost c: Set[Spec.K]) - returns (res: Bool, implicit ghost c1: Set[Spec.K]) - requires k in Spec.K.ks && nodeR(n, c) - ensures nodeR(n, c1) && Spec.opSpec(dop, k, c, c1, res) -} - -interface SearchStructure[K: Keyspace] { - module Spec = SearchStructureSpec[K] - type CSS - - pred cssR(r: CSS, c: Set[Spec.K]) - - inv cssInv(r: CSS) - - proc create() - returns (r: CSS) - ensures cssInv(r) && cssR(r, {||}) - - proc cssOp(dop: Spec.Op, r: CSS, k: Spec.K, implicit ghost c: Set[Spec.K]) - returns (res: Bool, implicit ghost c1: Set[Spec.K]) - requires k in Spec.K.ks && cssInv(r) - atomic requires cssR(r, c) - atomic ensures cssR(r, c1) && Spec.opSpec(dop, k, c, c1, res) -} - -module SingleNodeTemplate[K: Keyspace, Node: NodeImpl[K]] /* : SearchStructure[K] */ { - import Node - - module M_temp : Lib.Type { - rep type T = Set[Node.Spec.K] - } - - module FracSK = Lib.Frac[M_temp] - - type CSS = Ref - - - field lock: Lock - field node: Node - - //ghost fields - field cont_lock: FracSK - field cont_spec: FracSK - - pred nodePred(r: CSS, implicit ghost c: Set[Node.Spec.K]) { - Node.nodeR(r.node, c) && own(r.cont_lock, FracSK.frac_chunk(c, 1.0/2.0)) - } - - pred cssAuth(r: CSS, c: Set[Node.Spec.K]) { - own(r.cont_spec, FracSK.frac_chunk(c, 1.0/2.0)) - } - - pred cssR(r: CSS, c: Set[Node.Spec.K]) { - own(r.cont_spec, FracSK.frac_chunk(c, 1.0/2.0)) - } - - pred cssInv(r: CSS, implicit ghost b: Bool, implicit ghost c: Set[Node.Spec.K]) { - cssAuth(r, c) - && own(r.cont_lock, FracSK.frac_chunk(c, 1.0/2.0)) - && Lock.lock(r.lock, b) && (b ? true : nodePred(r)) - } - - proc create() - returns (r: CSS) - ensures cssInv(r) && cssR(r, {||}) - { - var l1: Lock; - l1 := Lock.create(); - var n: Node = Node.create(); - - r := new(lock:l1, node:n, cont_lock: FracSK.frac_chunk({||}, 1.0), cont_spec: FracSK.frac_chunk({||}, 1.0)); - - {! - fold cssAuth(r, {||}); - - fold nodePred(r); - - fold cssInv(r); - - fold cssR(r, {||}); - !} - } - - proc cssOp(dop: Node.Spec.Op, r: CSS, k: Node.Spec.K, implicit ghost c: Set[Node.Spec.K]) - returns (res: Bool, implicit ghost c1: Set[Node.Spec.K]) - requires k in Node.Spec.K.ks - requires cssInv(r) - requires cssR(r, c) - ensures cssR(r, c1) && Node.Spec.opSpec(dop, k, c, c1, res) - { - var b0: Bool = false; - var c0: Set[Node.Spec.K]; - - {! - unfold cssInv(r, b0, c0); - !} - - Lock.acquire(r.lock, b0); - - var c0_0: Set[Node.Spec.K]; - - {! - assert b0 == false; - assert nodePred(r); - fold cssInv(r, true, c0); - unfold nodePred(r, c0_0); - !} - - res, c1 := Node.decisiveOp(dop, r.node, k, c0_0); - - ghost var b1: Bool = true; - ghost var c1_0: Set[Node.Spec.K]; - - {! - assert cssInv(r, b1, c1_0); - unfold cssInv(r, b1, c1_0); - - fpu(r, cont_lock, FracSK.frac_chunk(c1, 1.0)); - - fold nodePred(r, c1); - - unfold cssAuth(r, c0_0); - unfold cssR(r, c); - - fpu(r, cont_spec, FracSK.frac_chunk(c1, 1.0)); - - fold cssAuth(r, c1); - fold cssR(r, c1); - - assert b1 == true; - assert Lock.lock(r.lock, true); - !} - - Lock.release(r.lock); - - {! - fold cssInv(r, false, c1); - !} - } -} diff --git a/test/concurrent/templates/single-node-test copy.rav b/test/concurrent/templates/single-node-test copy.rav deleted file mode 100644 index c490c22..0000000 --- a/test/concurrent/templates/single-node-test copy.rav +++ /dev/null @@ -1,342 +0,0 @@ -module Lock { - rep type T = Ref - - field bit: Bool - - pred lock(l: Ref, b: Bool) { - own(l.bit, b, 1.0) - } - - proc create() - returns (l: T) - ensures lock(l, false) - { - l := new(bit:false); - // l.bit := false; - - {! - fold lock(l, false); - !} - } - - proc acquire(l: T, implicit ghost b: Bool) - // atomic requires lock(l, b) - requires lock(l, b) - // atomic ensures lock(l, true) && b == false - ensures lock(l, true) // && b == false - { - {! - // var phi: AtomicToken; - // phi := bindAU(); - // var b: Bool; - // b := openAU(phi); - // inhale(lock(l,b)); - - // havoc b? - - unfold lock(l, b); - !} - - var res: Bool; - /* val res := cas(l.bit, false, true); */ - - if (l.bit) { /* can use l.bit OR b*/ - res := false; - } - - else { - res := true; - l.bit := true; - } - - {! - - if (res) { - fold lock(l, true); - // commitAU(phi); - assert (lock(l, true) && b == false); - } else { - fold lock(l, true); - // abortAU(phi); - assert(lock(l, b)); - } - !} - - if (!res) { - acquire(l, b); - } - } - - proc release(l: T) - // atomic requires lock(l, true) - // atomic ensures lock(l, false) - requires lock(l, true) - ensures lock(l, false) - { - {! - // var phi: AtomicToken; - // phi := bindAU(); - // openAU(phi); - unfold lock(l, true); - !} - - l.bit := false; - - {! - fold lock(l, false); - // commitAU(phi); - assert (lock(l, false)); - !} - } -} - - -interface Keyspace { - rep type T - val ks: Set[T] -} - -// module IntKeyspace : Keyspace { -// rep type T = Int - -// val ks: Set[T] = {| k: Int :: true |} -// } - -module SearchStructureSpec[K: Keyspace] { - - type Op = data { case searchOp; case insertOp; case deleteOp } - - pred opSpec(op: Op, k: K, c: Set[K], c1: Set[K], res: Bool) { - op == searchOp() ? - c1 == c && res == (k in c) : - (op == insertOp() ? - c1 == c ++ {|k|} && res == (k !in c) : - - // op == deleteOp - c1 == c -- {|k|} && res == (k in c) - ) - } -} - -interface NodeImpl[K: Keyspace] { - /* import K.ks */ - // import K - /* Need to figure out uppercase/lowercase for these commands.*/ - module Spec = SearchStructureSpec[K] - import Spec - - rep type T - - pred nodeR(n: T, c: Set[Spec.K]) - - proc create() - returns (n: T) - ensures nodeR(n, {||}) - - proc decisiveOp(dop: Spec.Op, n: T, k: Spec.K, implicit ghost c: Set[Spec.K]) - returns (res: Bool, implicit ghost c1: Set[Spec.K]) - // returns (res: DecisiveOpRet) - requires k in Spec.K.ks && nodeR(n, c) - ensures nodeR(n, c1) && Spec.opSpec(dop, k, c, c1, res) -} - -interface SearchStructure[K: Keyspace] { - /* import K.ks */ - // import K - module Spec = SearchStructureSpec[K] - // import Spec - - type CSS - - pred cssR(r: CSS, c: Set[Spec.K]) - - inv cssInv(r: CSS) - - proc create() - returns (r: CSS) - ensures cssInv(r) && cssR(r, {||}) - - proc cssOp(dop: Spec.Op, r: CSS, k: Spec.K, implicit ghost c: Set[Spec.K]) - returns (res: Bool, implicit ghost c1: Set[Spec.K]) - requires k in Spec.K.ks && cssInv(r) - atomic requires cssR(r, c) - atomic ensures cssR(r, c1) && Spec.opSpec(dop, k, c, c1, res) -} - -module SingleNodeTemplate[K: Keyspace, Node: NodeImpl[K]] /* : SearchStructure[K] */ { - // import K - import Node - - module M_temp : Lib.Type { - rep type T = Set[Node.Spec.K] - } - - module FracSK = Lib.Frac[M_temp] - - type CSS = Ref - - - field lock: Lock - field node: Node - - //ghost fields - field cont_lock: FracSK - field cont_spec: FracSK - - pred nodePred(r: CSS, implicit ghost c: Set[Node.Spec.K]) { - Node.nodeR(r.node, c) && own(r.cont_lock, FracSK.frac_chunk(c, 1.0/2.0)) - } - - pred cssAuth(r: CSS, c: Set[Node.Spec.K]) { - own(r.cont_spec, FracSK.frac_chunk(c, 1.0/2.0)) - } - - pred cssR(r: CSS, c: Set[Node.Spec.K]) { - own(r.cont_spec, FracSK.frac_chunk(c, 1.0/2.0)) - } - - pred cssInv(r: CSS, implicit ghost b: Bool, implicit ghost c: Set[Node.Spec.K]) { - cssAuth(r, c) - && own(r.cont_lock, FracSK.frac_chunk(c, 1.0/2.0)) - && Lock.lock(r.lock, b) && (b ? true : nodePred(r)) - } - - proc create() - returns (r: CSS) - ensures cssInv(r) && cssR(r, {||}) - { - var l1: Lock; - l1 := Lock.create(); - var n: Node = Node.create(); - - // var r: CSS; - r := new(lock:l1, node:n, cont_lock: FracSK.frac_chunk({||}, 1.0), cont_spec: FracSK.frac_chunk({||}, 1.0)); - - {! - /* check how dafny does it: uses assert */ - /* exists: false, {||} */ - - /* Not sure how symbolic execution is supposed to figure out where to apply this */ - // assert frac(1, {||}) == (frac(1/2, {||}) * frac(1/2, {||})); - - fold cssAuth(r, {||}); - - fold nodePred(r); - - // assert cssAuth(r, {||}) - // && own(r.cont_lock, {||}, 1.0/2.0) - // && Lock.lock(r.lock, b) && (b ? true : nodePred(r)); - fold cssInv(r); - /*createInv cssI cssInv(r);*/ - - fold cssR(r, {||}); - !} - } - - proc cssOp(dop: Node.Spec.Op, r: CSS, k: Node.Spec.K, implicit ghost c: Set[Node.Spec.K], implicit ghost l50: Ref) - returns (res: Bool, implicit ghost c1: Set[Node.Spec.K]) - requires k in Node.Spec.K.ks - requires own(r.lock, l50, 1.0) - // requires cssInv(r) - // atomic requires cssR(r, c) - // requires cssR(r, c) - // atomic ensures cssR(r, c1) && opSpec(dop, k, c, c1, res) - // ensures cssR(r, c1) && Node.Spec.opSpec(dop, k, c, c1, res) - { - var b0: Bool; - var c0: Set[Node.Spec.K]; - - {! - // unfold cssI; - inhale cssInv(r); - - // asserting above is useless for three reasons: - // 1. Currently asserting only checks whether stmt is valid. Does not actually assert it again to help the solver. This should be changed. - // 2. In the current implementation, predHeaps don't store implicit ghost variables. So b0, c0 are already being dropped before even asserting the pred. - - assume cssInv(r, b0, c0); - // EG: Even if we add implicit ghost vars to PredHeaps, how will that solve the binding problem? - - unfold cssInv(r, b0, c0); - - // fold Lock.lock(r.lock, b0); - // no need to fold since the lock is already given to us by the invariant. - !} - - // Lock.acquire(r.lock); - assert (exists b: Bool :: Lock.lock(r.lock,b)); - - var b1: Bool; - assume Lock.lock(r.lock,b1); - exhale Lock.lock(r.lock,b1); - - inhale Lock.lock(r.lock, true) && b1 == false; - - var c0_0: Set[Node.Spec.K]; - - {! - assert b0 == false; - assert nodePred(r); - // unfold Lock.lock(r.lock, true); - fold cssInv(r, true, c0); - unfold nodePred(r, c0_0); - !} - - // res, c1 := Node.decisiveOp(dop, r.node, k, c0_0); - exhale k in Node.Spec.K.ks && Node.nodeR(r.node,c); - inhale nodeR(r.node,c1) && Node.Spec.opSpec(dop, k, c0_0, c1, res); - - ghost var b2: Bool = true; - ghost var c1_0: Set[Node.Spec.K]; - - {! - // unfold cssInv; - assert cssInv(r, b2, c1_0); - unfold cssInv(r, b2, c1_0); - - /* lemma below asserts C0' = C1' - - lemma frac_eq(l: loc, ) - - */ - - // frac_eq((r.cont_lock), 1/2, 1/2, c0_0, c1_0); - - /* lemma below sums up fractional resources */ - // frac_sum((r.cont_lock), 1/2, 1/2, c0_0); - - /* lemma frac_update l C C' : - own(l.frac(1, C)) ~~> own(l.frac(1, C')) */ - fpu(r, cont_lock, FracSK.frac_chunk(c1, 1.0)); - - fold nodePred(r, c1); - - // val phi: AtomicToken; - // phi := bindAU(); - // c1_1 := openAU(phi); - - unfold cssAuth(r, c0_0); - unfold cssR(r, c); - - // frac_eq((r.cont_spec), 1/2, 1/2, c0_0, c); - // frac_sum((r.cont_spec), 1/2, 1/2, c0_0); - // frac_update((r.cont_spec), c0_0, c1); - - fpu(r, cont_spec, FracSK.frac_chunk(c1, 1.0)); - - fold cssAuth(r, c1); - fold cssR(r, c1); - // commitAU(phi); - - assert b2 == true; - assert Lock.lock(r.lock, true); - !} - - Lock.release(r.lock); - - {! - // unfold Lock.lock(r.lock, false); - fold cssInv(r, false, c1); - !} - } -} diff --git a/test/concurrent/templates/single-node-test.rav b/test/concurrent/templates/single-node-test.rav deleted file mode 100644 index b53c8c0..0000000 --- a/test/concurrent/templates/single-node-test.rav +++ /dev/null @@ -1,340 +0,0 @@ -module Lock { - rep type T = Ref - - field bit: Bool - - pred lock(l: Ref, b: Bool) { - own(l.bit, b, 1.0) - } - - proc create() - returns (l: T) - ensures lock(l, false) - { - l := new(bit:false); - // l.bit := false; - - {! - fold lock(l, false); - !} - } - - proc acquire(l: T, implicit ghost b: Bool) - // atomic requires lock(l, b) - requires lock(l, b) - // atomic ensures lock(l, true) && b == false - ensures lock(l, true) // && b == false - { - {! - // var phi: AtomicToken; - // phi := bindAU(); - // var b: Bool; - // b := openAU(phi); - // inhale(lock(l,b)); - - // havoc b? - - unfold lock(l, b); - !} - - var res: Bool; - /* val res := cas(l.bit, false, true); */ - - if (l.bit) { /* can use l.bit OR b*/ - res := false; - } - - else { - res := true; - l.bit := true; - } - - {! - - if (res) { - fold lock(l, true); - // commitAU(phi); - assert (lock(l, true) && b == false); - } else { - fold lock(l, true); - // abortAU(phi); - assert(lock(l, b)); - } - !} - - if (!res) { - acquire(l, b); - } - } - - proc release(l: T) - // atomic requires lock(l, true) - // atomic ensures lock(l, false) - requires lock(l, true) - ensures lock(l, false) - { - {! - // var phi: AtomicToken; - // phi := bindAU(); - // openAU(phi); - unfold lock(l, true); - !} - - l.bit := false; - - {! - fold lock(l, false); - // commitAU(phi); - assert (lock(l, false)); - !} - } -} - - -interface Keyspace { - rep type T - val ks: Set[T] -} - -// module IntKeyspace : Keyspace { -// rep type T = Int - -// val ks: Set[T] = {| k: Int :: true |} -// } - -module SearchStructureSpec[K: Keyspace] { - - type Op = data { case searchOp; case insertOp; case deleteOp } - - pred opSpec(op: Op, k: K, c: Set[K], c1: Set[K], res: Bool) { - op == searchOp() ? - c1 == c && res == (k in c) : - (op == insertOp() ? - c1 == c ++ {|k|} && res == (k !in c) : - - // op == deleteOp - c1 == c -- {|k|} && res == (k in c) - ) - } -} - -interface NodeImpl[K: Keyspace] { - /* import K.ks */ - // import K - /* Need to figure out uppercase/lowercase for these commands.*/ - module Spec = SearchStructureSpec[K] - import Spec - - rep type T - - pred nodeR(n: T, c: Set[Spec.K]) - - proc create() - returns (n: T) - ensures nodeR(n, {||}) - - proc decisiveOp(dop: Spec.Op, n: T, k: Spec.K, implicit ghost c: Set[Spec.K]) - returns (res: Bool, implicit ghost c1: Set[Spec.K]) - // returns (res: DecisiveOpRet) - requires k in Spec.K.ks && nodeR(n, c) - ensures nodeR(n, c1) && Spec.opSpec(dop, k, c, c1, res) -} - -interface SearchStructure[K: Keyspace] { - /* import K.ks */ - // import K - module Spec = SearchStructureSpec[K] - // import Spec - - type CSS - - pred cssR(r: CSS, c: Set[Spec.K]) - - inv cssInv(r: CSS) - - proc create() - returns (r: CSS) - ensures cssInv(r) && cssR(r, {||}) - - proc cssOp(dop: Spec.Op, r: CSS, k: Spec.K, implicit ghost c: Set[Spec.K]) - returns (res: Bool, implicit ghost c1: Set[Spec.K]) - requires k in Spec.K.ks && cssInv(r) - atomic requires cssR(r, c) - atomic ensures cssR(r, c1) && Spec.opSpec(dop, k, c, c1, res) -} - -module SingleNodeTemplate[K: Keyspace, Node: NodeImpl[K]] /* : SearchStructure[K] */ { - // import K - import Node - - module M_temp : Lib.Type { - rep type T = Set[Node.Spec.K] - } - - module FracSK = Lib.Frac[M_temp] - - type CSS = Ref - - - field lock: Lock - field node: Node - - //ghost fields - field cont_lock: FracSK - field cont_spec: FracSK - - pred nodePred(r: CSS, implicit ghost c: Set[Node.Spec.K]) { - Node.nodeR(r.node, c) && own(r.cont_lock, FracSK.frac_chunk(c, 1.0/2.0)) - } - - pred cssAuth(r: CSS, c: Set[Node.Spec.K]) { - own(r.cont_spec, FracSK.frac_chunk(c, 1.0/2.0)) - } - - pred cssR(r: CSS, c: Set[Node.Spec.K]) { - own(r.cont_spec, FracSK.frac_chunk(c, 1.0/2.0)) - } - - pred cssInv(r: CSS, implicit ghost b: Bool, implicit ghost c: Set[Node.Spec.K]) { - cssAuth(r, c) - && own(r.cont_lock, FracSK.frac_chunk(c, 1.0/2.0)) - && Lock.lock(r.lock, b) && (b ? true : nodePred(r)) - } - - proc create() - returns (r: CSS) - ensures cssInv(r) && cssR(r, {||}) - { - var l1: Lock; - l1 := Lock.create(); - var n: Node = Node.create(); - - // var r: CSS; - r := new(lock:l1, node:n, cont_lock: FracSK.frac_chunk({||}, 1.0), cont_spec: FracSK.frac_chunk({||}, 1.0)); - - {! - /* check how dafny does it: uses assert */ - /* exists: false, {||} */ - - /* Not sure how symbolic execution is supposed to figure out where to apply this */ - // assert frac(1, {||}) == (frac(1/2, {||}) * frac(1/2, {||})); - - fold cssAuth(r, {||}); - - fold nodePred(r); - - // assert cssAuth(r, {||}) - // && own(r.cont_lock, {||}, 1.0/2.0) - // && Lock.lock(r.lock, b) && (b ? true : nodePred(r)); - fold cssInv(r); - /*createInv cssI cssInv(r);*/ - - fold cssR(r, {||}); - !} - } - - proc cssOp(dop: Node.Spec.Op, r: CSS, k: Node.Spec.K, implicit ghost c: Set[Node.Spec.K]) - returns (res: Bool, implicit ghost c1: Set[Node.Spec.K]) - requires k in Node.Spec.K.ks - requires cssInv(r) - // atomic requires cssR(r, c) - requires cssR(r, c) - // atomic ensures cssR(r, c1) && opSpec(dop, k, c, c1, res) - ensures cssR(r, c1) && Node.Spec.opSpec(dop, k, c, c1, res) - { - var b0: Bool = false; - var c0: Set[Node.Spec.K]; - - {! - // unfold cssI; - // assert cssInv(r, b0, c0); - - // asserting above is useless for three reasons: - // 1. Currently asserting only checks whether stmt is valid. Does not actually assert it again to help the solver. This should be changed. - // 2. In the current implementation, predHeaps don't store implicit ghost variables. So b0, c0 are already being dropped before even asserting the pred. - - - unfold cssInv(r, b0, c0); - - // fold Lock.lock(r.lock, b0); - // no need to fold since the lock is already given to us by the invariant. - !} - - // Lock.acquire(r.lock); - - // var b: Bool; - Lock.acquire(r.lock, b0); - - // var b1: Bool - // assert exists b: Bool :: lock(l, b) - // (assert lock(l, b1)) - // exhale lock(l, b1) - - // inhale lock(l, b1) - - var c0_0: Set[Node.Spec.K]; - - {! - assert b0 == false; - assert nodePred(r); - // unfold Lock.lock(r.lock, true); - fold cssInv(r, true, c0); - unfold nodePred(r, c0_0); - !} - - res, c1 := Node.decisiveOp(dop, r.node, k, c0_0); - - ghost var b1: Bool = true; - ghost var c1_0: Set[Node.Spec.K]; - - {! - // unfold cssInv; - assert cssInv(r, b1, c1_0); - unfold cssInv(r, b1, c1_0); - - /* lemma below asserts C0' = C1' - - lemma frac_eq(l: loc, ) - - */ - - // frac_eq((r.cont_lock), 1/2, 1/2, c0_0, c1_0); - - /* lemma below sums up fractional resources */ - // frac_sum((r.cont_lock), 1/2, 1/2, c0_0); - - /* lemma frac_update l C C' : - own(l.frac(1, C)) ~~> own(l.frac(1, C')) */ - fpu(r, cont_lock, FracSK.frac_chunk(c1, 1.0)); - - fold nodePred(r, c1); - - // val phi: AtomicToken; - // phi := bindAU(); - // c1_1 := openAU(phi); - - unfold cssAuth(r, c0_0); - unfold cssR(r, c); - - // frac_eq((r.cont_spec), 1/2, 1/2, c0_0, c); - // frac_sum((r.cont_spec), 1/2, 1/2, c0_0); - // frac_update((r.cont_spec), c0_0, c1); - - fpu(r, cont_spec, FracSK.frac_chunk(c1, 1.0)); - - fold cssAuth(r, c1); - fold cssR(r, c1); - // commitAU(phi); - - assert b1 == true; - assert Lock.lock(r.lock, true); - !} - - Lock.release(r.lock); - - {! - // unfold Lock.lock(r.lock, false); - fold cssInv(r, false, c1); - !} - } -} diff --git a/test/concurrent/templates/single-node_working.rav b/test/concurrent/templates/single-node.rav similarity index 100% rename from test/concurrent/templates/single-node_working.rav rename to test/concurrent/templates/single-node.rav diff --git a/test/concurrent/templates/single-node.t b/test/concurrent/templates/single-node.t new file mode 100644 index 0000000..d515920 --- /dev/null +++ b/test/concurrent/templates/single-node.t @@ -0,0 +1,2 @@ + $ dune exec -- raven --shh ./single-node.rav + Verification successful. diff --git a/test/concurrent/templates/single-node_annoted.rav b/test/concurrent/templates/single-node_annoted.rav deleted file mode 100644 index ff9404c..0000000 --- a/test/concurrent/templates/single-node_annoted.rav +++ /dev/null @@ -1,426 +0,0 @@ -module Lock { - - field bit: Bool - - pred lock(l: Ref, b: Bool) { - own(l.bit, b) - } - - proc create() - returns (l: Ref) - ensures lock(l, false) - { - l := new bit(false); - - {! - fold lock(l, false); - !} - } - - proc acquire(l: Ref, implicit ghost b: Bool) - atomic requires lock(l, b) - atomic ensures lock(l, true) && b == false - { - // {{ AU(v_phi, "acquire", l, None, not_open) }} - - val phi: Perm; - - {! - phi := bindAU(); - - // {{ AU(v_phi, "acquire", l, None, not_open) }} * {{ phi = v_phi }} - - val b: Bool; - b := openAU(phi); - - // {{ AU(v_phi, "acquire", l, None, open(v_b)), lock(l, v_b) }} * - // {{ phi = v_phi, b = v_b }} - - unfold lock(l, b); - - // {{ AU(v_phi, "acquire", l, None, open(v_b)), own(l.bit, b) }} * - // {{ phi = v_phi, b = v_b }} - - !} - - /* Need to add CAS - - val res = cas(l.bit, false, true); - - CAS_SUCC : - {{ AU(v_phi, "acquire", l, None, open(v_b)), own(l.bit, b') }} * - {{ phi = v_phi, b = v_b, b = false, b' = true, res = true }} - - OR - - CAS_FAIL: - {{ AU(v_phi, "acquire", l, None, open(v_b)), own(l.bit, b') }} * - {{ phi = v_id, b = v_b, b != false, b' = b, res = false }} - - CAS_SUCC - -------- - - {{ AU(v_phi, "acquire", l, None, open(v_b)), own(l.bit, b') }} * - {{ phi = v_phi, b = false, b' = true, res = true }} - - */ - - {! - if (res) { - - // {{ AU(v_phi, "acquire", l, None, open(v_b)), own(l.bit, b') }} * - // {{ phi = v_phi, b = false, b' = true, res = true }} - - fold lock(l, true); - - // {{ AU(v_phi, "acquire", l, None, open(v_b)), lock(l, true) }} * - // {{ phi = v_phi, b = false, b' = true, res = true }} - - commitAU(phi, ()); - - /* - exhale post("acquire") - exhale (lock(l, true) &*& v_b == false) - */ - - // {{ AU(v_phi, "acquire", l, Some(()), not_open) }} * - // {{ phi = v_phi, b = false, b' = true, res = true }} - - } else { - fold lock(l, false); - abortAU(phi); - } - !} - - CAS_FAIL - -------- - - // {{ AU(v_phi, "acquire", l, None, open(v_b)), own(l.bit, b') }} * - // {{ phi = v_id, b = v_b, b != false, b' = b, res = false }} - - {! - if (res) { - fold lock(l, true); - commitAU(phi, ()); - } else { - - fold lock(l, true); - - // {{ AU(v_phi, "acquire", l, None, open(v_b)), lock(l, true) }} * - // {{ phi = v_id, b = v_b, b != false, b' = b, res = false }} - - abortAU(phi); - /* - exhale pre("acquire") with current pseudo_quant variables (lock(l, v_b)) - exhale (lock(l, v_b)) - */ - - // {{ AU(v_phi, "acquire", l, None, not_open) }} * - // {{ phi = v_id, b = v_b, b != false, b' = b, res = false }} - } - !} - - /* Check for unsoundness here */ - if (!res) { - - // {{ AU(v_phi, "acquire", l, None, not_open) }} * - // {{ phi = v_id, b = v_b, b != false, b' = b, res = false }} - - val b2: Bool; - b2 := openAU(phi); - - // {{ AU(v_phi, "acquire", l, None, open(v_b2)), lock(l, v_b2) }} * - // {{ phi = v_phi, b = v_b2 }} - - acquire(l); - - /* - exhale pre("acquire") with existential (exists b' :: lock(l, b')) - inhale post("acquire") (lock(l, true) &*& b' = false) - */ - - commit(phi) - - } - } - - proc release(l: Ref) - atomic requires lock(l, true) - atomic ensures lock(l, false) - { - val phi: Perm; - {! - phi := bindAU(); - openAU(phi); - unfold lock(l, true); - !} - - l.(Lock.bit) := false; - - {! - fold lock(l, true); - commitAU(phi); - !} - } -} - - -interface Keyspace { - rep type t - - val KS: Set[t] -} - -module IntKeyspace : Keyspace { - rep type t = Int - - val KS = {| k: Int :: true |} -} - -module SearchStructureSpec[K: Keyspace] { - - type Op = data { case searchOp ; case insertOp ; case deleteOp } - - pred opSpec(op: Op, k: K, c: Set[K], c': Set[K], res: Bool) { - if (op == searchOp) { - C' == C && res == (k in C) - } else if (op == insertOp) { - C' == C ++ {|k|} && res == (k !in C) - } else { - C' == C -- {|k|} && res == (k in C) - } - } -} - -interface NodeImpl[K: Keyspace] { - - /*import K.KS*/ - module Spec = SearchStructureSpec[K] - import Spec - - rep type t - - pred nodeR(n: T, c: Set[K]) - - proc create() - returns (n: T) - ensures nodeR(n, {||}) - - proc decisiveOp(dop: Op, n: T, k: K, implicit ghost c: Set[K]) - returns (res: Bool, implicit ghost c': Set[K]) - requires k in ks && nodeR(n, c) - ensures nodeR(n, c') && opSpec(dop, k, c, c', res) -} - -interface SearchStructure[K: Keyspace] { - /* import K.KS */ - module Spec = SearchStructureSpec[K] - import Spec - - /* css or Ref? */ - type css - - pred cssR(r: css, c: Set[K]) - - inv cssInv(r: css) - - proc create() - returns (r: css) - ensures cssInv(cssI, cssInv(r)) && cssR(r, {||}) - - proc cssOp(dop: Op, r: CSS, k: K, implicit ghost c: Set[K]) - returns (res: Bool, implicit ghost c': Set[K]) - requires k in ks - requires cssInv(r) - atomic requires cssR(r, c) - atomic ensures cssR(r, c') && opSpec(dop, k, c, c', res) -} - -module SingleNodeTemplate[K: Keyspace, Node: NodeImpl[K]] : SearchStructure[K] { - /* import K.KS */ - import Node - - module FracSK = Frac[K.KS] - module AgreeAD = Agree[Addresses]; - - field lock: Ref; - field lock_ag: AgreeAD; - field node: Ref; - field node_ag: AgreeAD; - field cont_lock: FracSK; - field cont_spec: FracSK; - - pred nodePred(r: css) { - exists c: Set[K] :: nodeR(r.node, c) && own(r.cont_lock.frac(1/2, c)) - } - - pred cssAuth(r: css, c: Set[K]) { - own(r.cont_spec.frac(1/2, c)) - } - - pred cssR(r: css, c: Set[K]) { - own(r.cont_spec.frac(1/2, c)) - } - - inv cssInv(r: css) { - exists b: Bool, c: Set[K], l: Ref :: - cssAuth(r, c) - && own(r.cont_lock.frac(1/2, c)) - && own(r.lock, l) - && Lock.lock(l, b) && (b ? true : nodePred(r)) - } - - proc create() - returns (r: css) - ensures cssR(r, {||}) &*& cssInv(r) - { - val l: Ref = Lock.create(); - val n: Node = Node.create(); - - {{ Lock.lock(l, false), nodeR(n, {||}) }} - - val r: css; - - r.lock := l; - r.node := n; - r.cont_lock := frac(1, {||}); - r.cont_spec := frac(1, {||}); - - {{ Lock.lock(l, false), nodeR(n, {||}), own(r.lock.l), own(r.node.n), - own(r.cont_lock.frac(1, {||})), own(r.cont_spec.frac(1, {||})) }} - - {! - - /* symb_exec first checks if frac(1/2, {||}) <= frac(1, {||}) */ - /* After, [ frame (frac(1, {||})) (frac(1/2, {||})) ] remains */ - fold(cssAuth(r, {||})); - - {{ Lock.lock(l, false), nodeR(n, {||}, own(r.lock.l), own(r.node.n), - own(r.cont_lock.frac(1, {||})), own(r.cont_spec.frac(1/2, {||})), - cssAuth(r, {||}) }} - - assert nodeR(r.node, {||}) &*& own(r.cont_lock.frac(1/2, {||})) - - fold nodePred(r) - - {{ Lock.lock(l, false), own(r.lock.l), own(r.node.n), - own(r.cont_lock.frac(1/2, {||})), own(r.cont_spec.frac(1/2, {||})), - cssAuth(r, {||}), nodePred(r) }} - - - assert cssAuth(r, {||}) &*& own(r.cont_lock.frac(1/2, {||})) - &*& Lock.lock(r.lock, false) &*& (false ? true : nodePred(r)); - - fold cssInv(r); - - {{ cssInv(r), own(r.cont_spec.frac(1/2, {||})) }} - - fold cssR(r, {||}); - - {{ cssInv(r), cssR(r, {||}) }} - - !} - } - - proc cssOp(dop: Op, r: CSS, k: K, implicit ghost c: Set[K]) - returns (res: Bool, implicit ghost c': Set[K]) - requires k in ks - requires cssInv(r) - atomic requires cssR(r, c) - atomic ensures cssR(r, c') &*& opSpec(dop, k, c, c', res) - { - {! - - {{ cssInv(r) }} - - openInv cssInv(r); - - {{ cssAuth(r, v_c), own(r.cont_lock.frac(1/2, v_c)), - own(r.lock.v_l), Lock.lock(v_l, v_b), (v_b ? true : nodePred(r)) }} - - var b0, c0, l :| cssAuth(r, c) &*& own(r.lock.l) &*& Lock.lock(l, b) - - {{ cssAuth(r, v_c), own(r.cont_lock.frac(1/2, v_c)), - own(r.lock.v_l), Lock.lock(v_l, v_b), (v_b ? true : nodePred(r)) }} * - {{ b0 = v_b, c0 = v_c, l = v_l }} - - !} - - var l = r.lock; - acquire(l); - - {{ cssAuth(r, v_c), own(r.cont_lock.frac(1/2, v_c)), - own(r.lock.v_l), Lock.lock(v_l, true), nodePred(r) }} * - {{ b0 = v_b, c0 = v_c, l = v_l }} - - {! - - assert cssAuth(r, c0) &*& own(r.lock.l) &*& Lock.lock(r.lock, true); - - closeInv cssInv(r); - - {{ nodePred(r) }} - - assert nodePred(r); - unfold nodePred(r); - - {{ nodeR(r.node, v_c1), own(r.cont_lock.frac(1/2, v_c1)) }} - - !} - - res, c1 := decisiveOp(dop, r.node, k); - - {{ nodeR(n, c1), own(r.cont_lock.frac(1/2, v_c1) }} * - {{ opSpec(dop, k, c1, v_c1, res) }} - - - - {! - unfold cssI; - /* unfold (b1, C1')cssInv(r); */ - unfold cssInv(r); - - /* lemma below asserts C0' = C1' - - lemma frac_eq(l: loc, ) - - */ - frac_eq((r.cont_lock), 1/2, 1/2, c0', c1'); - - /* lemma below sums up fractional resources */ - frac_sum((r.cont_lock), 1/2, 1/2, c0'); - - /* lemma frac_update l C C' : - own(l.frac(1, C)) ~~> own(l.frac(1, C')) */ - frac_update((r.cont_lock), c0', c1); - - /* fold (C1)nodePred(r) */ - fold nodePred(r); - - phi, c1'' := openAU; - - unfold cssAuth(r, c0'); - unfold cssR(r, c1''); - frac_eq((r.cont_spec), 1/2, 1/2, c0', c1''); - frac_sum((r.cont_spec), 1/2, 1/2, c0'); - frac_update((r.cont_spec), c0', c1); - - fold cssAuth(r, c1); - fold cssR(r, c1); - commit(phi); - - assert b1 == true; - fold Lock.lock(r, true); - !} - - release(r.lock); - - {! - unfold Lock.lock(r, false); - /* fold (false, C1)cssInv(r); */ - fold cssInv(r); - fold cssI; - !} - } -} - diff --git a/test/concurrent/templates/single-node_imports.rav b/test/concurrent/templates/single-node_imports.rav deleted file mode 100644 index 031319f..0000000 --- a/test/concurrent/templates/single-node_imports.rav +++ /dev/null @@ -1,304 +0,0 @@ -module Lock { - rep type T = Ref - - field bit: Bool - - pred lock(l: Ref, b: Bool) { - own(l.bit, b, 1.0) - } - - proc create() - returns (l: T) - ensures lock(l, false) - { - l := new(bit:false); - // l.bit := false; - - {! - fold lock(l, false); - !} - } - - proc acquire(l: T, implicit ghost b: Bool) - // atomic requires lock(l, b) - requires lock(l, b) - // atomic ensures lock(l, true) && b == false - ensures lock(l, true) && b == false - { - {! - // var phi: AtomicToken; - // phi := bindAU(); - // var b: Bool; - // b := openAU(phi); - // inhale(lock(l,b)); - - unfold lock(l, b); - !} - - var res: Bool; - /* val res := cas(l.bit, false, true); */ - - if (l.bit) { /* can use l.bit OR b*/ - res := false; - } - - else { - res := true; - } - - {! - if (res) { - fold lock(l, true); - // commitAU(phi); - assert (lock(l, true) && b == false); - } else { - fold lock(l, false); - // abortAU(phi); - assert(lock(l, b)); - } - !} - - if (!res) { - acquire(l); - } - } - - proc release(l: T) - // atomic requires lock(l, true) - // atomic ensures lock(l, false) - requires lock(l, true) - ensures lock(l, false) - { - {! - // var phi: AtomicToken; - // phi := bindAU(); - // openAU(phi); - unfold lock(l, true); - !} - - l.bit := false; - - {! - fold lock(l, true); - // commitAU(phi); - assert (lock(l, false)); - !} - } -} - - -interface Keyspace { - rep type T - val ks: Set[T] -} - -module IntKeyspace : Keyspace { - rep type T = Int - - val ks: Set[T] = {| k: Int :: true |} -} - -module SearchStructureSpec[K: Keyspace] { - - type Op = data { case searchOp; case insertOp; case deleteOp } - - pred opSpec(op: Op, k: K, c: Set[K], c1: Set[K], res: Bool) { - op == searchOp() ? - c1 == c && res == (k in c) : - (op == insertOp() ? - c1 == c ++ {|k|} && res == (k !in c) : - - // op == deleteOp - c1 == c -- {|k|} && res == (k in c) - ) - } -} - -interface NodeImpl[K: Keyspace] { - /* import K.ks */ - // import K - /* Need to figure out uppercase/lowercase for these commands.*/ - module Spec = SearchStructureSpec[K] - import Spec - - rep type T - - pred nodeR(n: T, c: Set[K]) - - proc create() - returns (n: T) - ensures nodeR(n, {||}) - - proc decisiveOp(dop: Op, n: T, k: K, implicit ghost c: Set[K]) - returns (res: Bool, implicit ghost c1: Set[K]) - requires k in K.ks && nodeR(n, c) - ensures nodeR(n, c1) && opSpec(dop, k, c, c1, res) -} - -interface SearchStructure[K: Keyspace] { - /* import K.ks */ - // import K - module Spec = SearchStructureSpec[K] - // import Spec - - type CSS - - pred cssR(r: CSS, c: Set[Spec.K]) - - inv cssInv(r: CSS) - - proc create() - returns (r: CSS) - ensures cssInv(r) && cssR(r, {||}) - /* What does `inv(cssI, cssInv(r))` mean? */ - - proc cssOp(dop: Spec.Op, r: CSS, k: Spec.K, implicit ghost c: Set[Spec.K]) - returns (res: Bool, implicit ghost c1: Set[Spec.K]) - requires k in Spec.K.ks && cssInv(r) - atomic requires cssR(r, c) - atomic ensures cssR(r, c1) && Spec.opSpec(dop, k, c, c1, res) -} - -module SingleNodeTemplate[K: Keyspace, Node: NodeImpl[K]] : SearchStructure[K] { - // import K - import Node - - module M_temp : Lib.Type { - rep type T = Set[K] - } - - module FracSK = Lib.Frac[M_temp] - - type CSS = Ref - - - field lock: Lock - field node: Node - - //ghost fields - field cont_lock: FracSK - field cont_spec: FracSK - - - pred nodePred(r: CSS, implicit ghost c: Set[K]) { - nodeR(r.node, c) && own(r.cont_lock, FracSK.frac_chunk(c, 1.0/2.0)) - } - - pred cssAuth(r: CSS, c: Set[Node.Spec.K]) { - own(r.cont_spec, FracSK.frac_chunk(c, 1.0/2.0)) - } - - pred cssR(r: CSS, c: Set[Node.Spec.K]) { - own(r.cont_spec, FracSK.frac_chunk(c, 1.0/2.0)) - } - - pred cssInv(r: CSS, implicit ghost b: Bool, implicit ghost c: Set[Node.Spec.K]) { - cssAuth(r, c) - && own(r.cont_lock, FracSK.frac_chunk(c, 1.0/2.0)) - && Lock.lock(r.lock, b) && (b ? true : nodePred(r)) - } - - proc create() - returns (r: CSS) - { - var l: Lock = Lock.create(); - var n: Node = Node.create(); - - var r: CSS; - r := new(lock:l, node:n, cont_lock: FracSK.frac_chunk({||}, 1.0), cont_spec: FracSK.frac_chunk({||}, 1.0)); - - // var r: CSS = new(lock(l), node(n), cont_lock(frac(1, {||})), cont_spec(frac(1, {||}))) - - {! - /* check how dafny does it: uses assert */ - /* exists: false, {||} */ - - /* Not sure how symbolic execution is supposed to figure out where to apply this */ - // assert frac(1, {||}) == (frac(1/2, {||}) * frac(1/2, {||})); - - fold(cssAuth(r, {||})); - - // assert cssAuth(r, {||}) - // && own(r.cont_lock, {||}, 1.0/2.0) - // && Lock.lock(r.lock, b) && (b ? true : nodePred(r)); - fold(cssInv(r)); - /*createInv cssI cssInv(r);*/ - - fold cssR(r, {||}); - !} - } - - proc cssOp(dop: Node.Spec.Op, r: CSS, k: Node.Spec.K, implicit ghost c: Set[K]) - returns (res: Bool, implicit ghost c1: Set[K]) - { - var b0: Bool; - var c0: Set[Node.Spec.K]; - - {! - // unfold cssI; - assert cssInv(r, b0, c0); - unfold cssInv(r, b0, c0); - fold Lock.lock(r.lock, b0); - !} - - Lock.acquire(r.lock); - - var c0_0: Set[Node.Spec.K]; - - {! - assert b0 == false; - assert nodePred(r); - unfold Lock.lock(r.lock, true); - fold cssInv(r, true, c0); - unfold nodePred(r, c0_0); - !} - - res, c1 := Node.decisiveOp(dop, r.node, k); - - {! - unfold cssInv; - unfold cssInv(r, b1, c1_0); - - /* lemma below asserts C0' = C1' - - lemma frac_eq(l: loc, ) - - */ - - frac_eq((r.cont_lock), 1/2, 1/2, c0_0, c1_0); - - /* lemma below sums up fractional resources */ - frac_sum((r.cont_lock), 1/2, 1/2, c0_0); - - /* lemma frac_update l C C' : - own(l.frac(1, C)) ~~> own(l.frac(1, C')) */ - frac_update((r.cont_lock), c0_0, c1); - - fold nodePred(r, c1); - - val phi: AtomicToken; - phi := bindAU(); - c1_1 := openAU(phi); - - unfold cssAuth(r, c0_0); - unfold cssR(r, c1_1); - frac_eq((r.cont_spec), 1/2, 1/2, c0_0, c1_1); - frac_sum((r.cont_spec), 1/2, 1/2, c0_0); - frac_update((r.cont_spec), c0_0, c1); - - fold cssAuth(r, c1); - fold cssR(r, c1); - commitAU(phi); - - assert b1 == true; - fold Lock.lock(r, true); - !} - - release(r.lock); - - {! - unfold Lock.lock(r, false); - fold cssInv(r, false, c1); - !} - } -} diff --git a/test/concurrent/templates/single-node_rough.rav b/test/concurrent/templates/single-node_rough.rav deleted file mode 100644 index dc127f7..0000000 --- a/test/concurrent/templates/single-node_rough.rav +++ /dev/null @@ -1,282 +0,0 @@ -module Lock { - rep type t = struct { - var bit: Bool - } - - pred lock(l: t, b: Bool) { - own(l.bit, b) - } - - proc create() - returns (l: t) - ensures lock(l, false) - { - l := new t; - l.bit := false; - - {! - fold lock(l, false); - !} - } - - proc acquire(l: t, implicit ghost b: Bool) - atomic requires lock(l, b) - atomic ensures lock(l, true) && b == false - { - {! - var phi: AtomicToken; - phi := bindAU(); - var b: Bool; - b := openAU(phi); - - unfold lock(l, b); - !} - - var res: Bool; - /* val res := cas(l.bit, false, true); */ - - if (l.bit) { /* can use l.bit OR b*/ - res := false; - } - - else { - res := true; - } - - {! - if (res) { - fold lock(l, true); - commitAU(phi); - } else { - fold lock(l, false); - abortAU(phi); - } - !} - - if (!res) { - acquire(l); - } - } - - proc release(l: t) - atomic requires lock(l, true) - atomic ensures lock(l, false) - { - {! - var phi: AtomicToken; - phi := bindAU(); - openAU(phi); - unfold lock(l, true); - !} - - l.bit := false; - - {! - fold lock(l, true); - commitAU(phi); - !} - } -} - - -interface Keyspace { - rep type t - val ks: Set[t] -} - -module IntKeyspace : Keyspace { - rep type t = Int - - val ks = {| k: Int :: true |} -} - -module SearchStructureSpec[K: Keyspace] { - - type op = data { case searchOp; case insertOp; case deleteOp } - -/* pred opSpec(op: op, k: K, c: Set[K], c': Set[K], res: Bool) { - match(op) { - case searchOp => C' == C && res == (k in C) - case insertOp => C' == C ++ {|k|} && res == (k !in C) - case insertOp => C' == C -- {|k|} && res == (k in C) - } - } */ -} - -interface NodeImpl[K: Keyspace] { - /* import K.ks */ - import K - /* Need to figure out uppercase/lowercase for these commands.*/ - module Spec = SearchStructureSpec[K] - import Spec - - rep type t - - pred nodeR(n: t, c: Set[k]) - - proc create() - returns (n: t) - ensures nodeR(n, {||}) - - proc decisiveOp(dop: op, n: t, k: k, implicit ghost c: Set[k]) - returns (res: Bool, implicit ghost c': Set[k]) - requires k in ks && node(n, c) - ensures nodeR(n, c') && opSpec(dop, k, c, c', res) -} - -interface SearchStructure[K: Keyspace] { - /* import K.ks */ - import K - module Spec = SearchStructureSpec[K] - import Spec - - type css - - pred cssR(r: css, c: Set[K]) - - inv cssInv(r: CSS) - - proc create() - returns (r: CSS) - ensures cssInv(r) && cssR(r, {||}) - /* What does `inv(cssI, cssInv(r))` mean? */ - - proc cssOp(dop: op, r: css, k: K, implicit ghost c: Set[K]) - returns (res: Bool, implicit ghost c': Set[K]) - requires k in ks && cssInv(r) - atomic requires cssR(r, c) - atomic ensures cssR(r, c') && opSpec(dop, k, c, c', res) -} - -module SingleNodeTemplate[K: Keyspace, Node: NodeImpl[K]] : SearchStructure[K] { - import K - import Node - - module FracSK = Frac[Set[K]] - - type css = struct { - var lock: Lock - var node: Node - ghost var cont_lock: FracSK - ghost var cont_spec: FracSK - } - - pred nodePred(r: css, implicit ghost c: Set[K]) { - nodeR(r.node, c) && own(r.cont_lock.frac(1/2, c)) - } - - pred cssAuth(r: css, c: Set[K]) { - own(r.cont_spec.frac(1/2, c)) - } - - pred cssR(r: css, c: Set[K]) { - own(r.cont_spec.frac(1/2, c)) - } - - pred cssInv(r: css, implicit ghost b: Bool, implicit ghost c: Set[K]) { - cssAuth(r, c) - && own(r.cont_lock.frac(1/2, c)) - && Lock.lock(r.lock, b) && (b ? true : nodePred(r)) - } - - proc create() - returns (r: css) - { - var l: Lock = Lock.create(); - var n: Node = Node.create(); - - var r: CSS = new css; - r.lock := l; - r.node := n; - r.cont_lock := frac(1, {||}); - r.cont_spec := (frac(1, {||})); - - /*var r: CSS = new(lock(l), node(n), cont_lock(frac(1, {||})), cont_spec(frac(1, {||})) */ - - {! - /* check how dafny does it: uses assert */ - /* exists: false, {||} */ - - /* Not sure how symbolic execution is supposed to figure out where to apply this */ - assert frac(1, {||}) == (frac(1/2, {||}) * frac(1/2, {||})); - - fold(cssAuth(r, {||})); - - assert cssAuth(r, c) - && own(r.cont_lock.frac(1/2, c)) - && Lock.lock(r.lock, b) && (b ? true : nodePred(r)); - fold(cssInv(r)); - /*createInv cssI cssInv(r);*/ - - fold cssR(r, {||}); - !} - } - - proc cssOp(dop: op, r: css, k: K, implicit ghost c: Set[K]) - returns (res: Bool, implicit ghost c': Set[K]) - { - {! - unfold cssI; - unfold cssInv(r, b0, c0); - fold Lock.lock(r.lock, b0); - !} - - acquire(r.lock); - - {! - assert b0 == false; - assert nodePred(r); - unfold Lock.lock(r.lock, true); - fold cssInv(r, true, c0); - unfold nodePred(r, c0'); - !} - - res, c1 := decisiveOp(dop, r, k); - - {! - unfold cssInv; - unfold cssInv(r, b1, c1'); - - /* lemma below asserts C0' = C1' - - lemma frac_eq(l: loc, ) - - */ - - frac_eq((r.cont_lock), 1/2, 1/2, c0', c1'); - - /* lemma below sums up fractional resources */ - frac_sum((r.cont_lock), 1/2, 1/2, c0'); - - /* lemma frac_update l C C' : - own(l.frac(1, C)) ~~> own(l.frac(1, C')) */ - frac_update((r.cont_lock), c0', c1); - - fold nodePred(r, c1); - - val phi: AtomicToken; - phi := bindAU(); - c1'' := openAU(phi); - - unfold cssAuth(r, c0'); - unfold cssR(r, c1''); - frac_eq((r.cont_spec), 1/2, 1/2, c0', c1''); - frac_sum((r.cont_spec), 1/2, 1/2, c0'); - frac_update((r.cont_spec), c0', c1); - - fold cssAuth(r, c1); - fold cssR(r, c1); - commitAU(phi); - - assert b1 == true; - fold Lock.lock(r, true); - !} - - release(r.lock); - - {! - unfold Lock.lock(r, false); - fold cssInv(r, false, c1); - !} - } -} diff --git a/test/concurrent/templates/single-node_working.t b/test/concurrent/templates/single-node_working.t deleted file mode 100644 index c933737..0000000 --- a/test/concurrent/templates/single-node_working.t +++ /dev/null @@ -1,2 +0,0 @@ - $ dune exec -- raven --shh ./single-node_working.rav - Verification successful. diff --git a/test/concurrent/treiber_stack/treiber_stack_rewritten.rav b/test/concurrent/treiber_stack/treiber_stack_rewritten.rav index 34bc374..4578519 100644 --- a/test/concurrent/treiber_stack/treiber_stack_rewritten.rav +++ b/test/concurrent/treiber_stack/treiber_stack_rewritten.rav @@ -105,7 +105,7 @@ proc pop(s: Ref, implicit ghost xs: IntList) if (hd == null) { // assert false; unfold is_list(hd, xs0); - fold is_list(hd, xs0); + fold is_list(hd, xs0)[q := 0.0]; fold is_stack(s, xs0); // commitAU(phi, none()); var result0: IntOption := none(); diff --git a/test/iterated-star/binary-graph.rav b/test/iterated-star/binary-graph.rav deleted file mode 100644 index f14343a..0000000 --- a/test/iterated-star/binary-graph.rav +++ /dev/null @@ -1,59 +0,0 @@ -field first : Ref -field second : Ref - -proc inc(nodes: Set[Ref], x: Ref) returns (y: Ref) - requires forall n: Ref :: n in nodes ==> own(n.first.(1, Mf[n])) - requires forall n: Ref :: n in nodes ==> (Mf[n] != null ==> Mf[n] in nodes) - requires forall n: Ref :: n in nodes ==> own(n.second.(1, Ms[n])) - requires forall n: Ref :: n in nodes ==> (Ms[n] != null ==> Ms[n] in nodes) - requires x in nodes - ensures y != null ==> y in nodes -{ - if(x.second != null) { - y := x.second.first - } -} - -(* fail *) -proc inc2(nodes: Set[Ref], x: Ref) returns (y: Ref) - requires forall n: Ref :: n in nodes ==> own(n.first.(1, Mf[n])) - requires forall n: Ref :: n in nodes ==> (Mf[n] != null ==> Mf[n] in nodes) - requires forall n: Ref :: n in nodes ==> own(n.second.(1, Ms[n])) - requires x in nodes - ensures y != null ==> y in nodes -{ - if(x.second != null) { - y := x.second.first - } -} - -(* pass *) -proc inc3(nodes: Set[Ref], x: Ref) returns (y: Ref) - requires forall n: Ref :: n in nodes ==> own(n.first.(1, Mf[n])) - requires forall n: Ref :: n in nodes ==> (Mf[n] in nodes) - requires forall n: Ref :: n in nodes ==> own(n.second.(1, Ms[n])) - requires forall n: Ref :: n in nodes ==> (Ms[n] != null ==> Ms[n] in nodes) - requires x in nodes - ensures y != null ==> y in nodes -{ - if(x.second != null) { - y := x.second.first - assert y != null - } -} - -(* fail *) -proc inc4(nodes: Set[Ref], x: Ref) returns (y: Ref) - requires forall n: Ref :: n in nodes ==> own(n.first.(1, Mf[n])) - requires forall n: Ref :: n in nodes ==> (Mf[n] != null ==> Mf[n] in nodes) - requires forall n: Ref :: n in nodes ==> own(n.second.(1, Ms[n])) - requires forall n: Ref :: n in nodes ==> (Ms[n] != null ==> Ms[n] in nodes) - requires x in nodes - ensures y != null ==> y in nodes -{ - if(x.second != null) { - y := x.second.first - // this assert fails - assert y != null - } -} diff --git a/test/iterated-star/binary-graph2.rav b/test/iterated-star/binary-graph2.rav deleted file mode 100644 index 36e8c2e..0000000 --- a/test/iterated-star/binary-graph2.rav +++ /dev/null @@ -1,54 +0,0 @@ -field val : Ref - -(* pass *) -proc difference(nodes1: Set[Ref], nodes2: Set[Ref]) - requires forall n: Ref :: n in nodes1 ==> own(n.val, M(n)) - requires nodes1 subsetof nodes2 - ensures forall n: Ref :: n in nodes2 ==> own(n.val, M(n)) - ensures forall n: Ref :: n in nodes1 -- nodes2 ==> own(n.val, M(n)) -{ -} - -(* pass *) -proc inc1(nodes: Set[Ref], x: Ref) returns (new_nodes: Set[Ref]) - requires forall n: Ref :: n in nodes ==> own(n.val, _) - requires x !in nodes - requires own(x.val, _) - ensures new_nodes == nodes ++ { x } - ensures forall n: Ref :: n in new_nodes ==> own(n.val, _) -{ - new_nodes := nodes ++ { x } -} - -(* fail *) -proc inc2(nodes: Set[Ref], x: Ref) returns (new_nodes: Set[Ref]) - requires forall n: Ref :: n in nodes ==> own(n.val, _) - requires x !in nodes - ensures new_nodes == nodes ++ { x } - ensures forall n: Ref :: n in new_nodes ==> own(n.val, _) -{ - new_nodes := nodes ++ { x } -} - -(* pass *) -proc dec1(nodes: Set[Ref], x: Ref) returns (new_nodes: Set[Ref]) - requires forall n: Ref :: n in nodes ==> own(n.val, _) - requires x in nodes - ensures new_nodes == nodes -- { x } - ensures forall n: Ref :: n in new_nodes ==> own(n.val, _) - ensures own(x.val, _) -{ - new_nodes := nodes -- { x } -} - -(* pass *) -proc union(nodes1: Set[Ref], nodes2: Set[Ref]) returns (new_nodes: Set[Ref]) - requires forall n: Ref :: n in nodes1 ==> own(n.val, _) - requires forall n: Ref :: n in nodes2 ==> own(n.val, _) - ensures new_nodes == nodes1 ++ nodes2 - ensures forall n: Ref :: n in new_nodes ==> own(n.val, M(n)) -{ - new_nodes := nodes1 ++ nodes -} - - diff --git a/test/iterated-star/receiver-expr.rav b/test/iterated-star/receiver-expr.rav deleted file mode 100644 index 6f0a295..0000000 --- a/test/iterated-star/receiver-expr.rav +++ /dev/null @@ -1,36 +0,0 @@ -field val : Int - -func address(i: Int) returns (r: Ref) - -lemma address_disj(i: Int, j: Int) - ensures i != j ==> address(i)!=address(j) - -proc test() -{ - inhale own(address(3).val.(1/2, _)) - inhale own(address(2).val.(1/2, _)) - inhale own(address(1).val.(1/2, _)) - exhale forall i: Int :: 1 <= i <= 3 ==> own(address(i).val.(1/2, _)) -} - -func address2(i: Int) returns (r: Ref) - -proc test2() -{ - inhale own(address2(3).val.(1, _)) - inhale own(address2(2).val.(1, _)) - inhale own(address2(1).val.(1, _)) - exhale forall i: Int :: 1 <= i <= 3 ==> own(address2(i).val.(1/2, _)) -} - -func address3(i: Int) returns (r: Ref) - -proc test3() -{ - inhale own(address3(3).val.(1/2, _)) - inhale own(address3(2).val.(1/2, _)) - inhale own(address3(1).val.(1/2, _)) - inhale address3(1) != address3(2) && address3(2) != address3(3) && address3(3) != address3(1) - exhale forall i: Int :: 1 <= i <= 3 ==> own(address3(i).val.(1/2, _)) -} - diff --git a/test/list_predicates2.rav b/test/linked-lists/list_predicates2_wip.rav similarity index 100% rename from test/list_predicates2.rav rename to test/linked-lists/list_predicates2_wip.rav diff --git a/test/list_predicates.rav b/test/linked-lists/list_predicates_wip.rav similarity index 100% rename from test/list_predicates.rav rename to test/linked-lists/list_predicates_wip.rav diff --git a/todo.md b/todo.md index ed9720e..fd629cf 100644 --- a/todo.md +++ b/todo.md @@ -1,3 +1,7 @@ +16 nov, 2024: +- fix ident sanitization bug identified by Lucas. +- move statistics counting to after type-checking for greater accuracy. + 22 oct, 2024: - fix bug with existenials occuring in other variables' skolem function + [x] rewrite the entire elim_a functionality. @@ -6,14 +10,15 @@ - [x] exhale order of clause witness computation bug - [x] formalize masks -- introduce fold existential witness notation +- [x] introduce fold existential witness notation -- move injectivity check outside. +- [x] move injectivity check outside. - reorder rewrite passes to do inj checks for preds before rewriting fold/unfold - maybe by adding new lemmas + + maybe by adding new lemmas - sweep to add default triggers for every Quant + + fix missing triggers in all `Expr.mk_binder` calls -- add forks +- [x] add forks - toy around with preds as macros @@ -31,13 +36,10 @@ Type-checking: - Revamp witness computation code - [x] Fix `return proc()` stmts -- Allow parsing of `map[m1][m2]` expressions - iirc Thomas did implement a fix for this, but he thinks it was a bit hacky. +- [x] Allow parsing of `map[m1][m2]` expressions + (Thomas did implement a fix for this, but needs review) - Parse field reads/writes/cas/fpu separately - -- Fix missing triggers in all `Expr.mk_binder` calls - - Allow types to be used as modules implementing Library.Type @@ -45,11 +47,4 @@ Type-checking: === - [x] Fix dependency analysis wrt auto lemmas -- [x] Investigate spurious "unknown"s in the middle of log files - - -pred(a,b) { - \exists x^123, y :: -} - -fold pred(a_1, a_2)[x := ..., x := ] \ No newline at end of file +- [x] Investigate spurious "unknown"s in the middle of log files \ No newline at end of file