From a0e17f9c2e4fa75b932d18d358a384b2eec86754 Mon Sep 17 00:00:00 2001 From: Thomas Wies Date: Fri, 22 Nov 2024 20:14:59 -0500 Subject: [PATCH] towards simplified give-up template --- .../concurrent/templates/give-up-lock_wip.rav | 53 +- .../templates/give-up-simplified.rav | 549 ++++++++++++++++++ 2 files changed, 575 insertions(+), 27 deletions(-) create mode 100644 test/concurrent/templates/give-up-simplified.rav diff --git a/test/concurrent/templates/give-up-lock_wip.rav b/test/concurrent/templates/give-up-lock_wip.rav index 652eeb7..a51e233 100644 --- a/test/concurrent/templates/give-up-lock_wip.rav +++ b/test/concurrent/templates/give-up-lock_wip.rav @@ -24,12 +24,12 @@ interface SearchStructureSpec { 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) { + func opSpec(op: Op, k: K, c_in: Set[K]) returns (c_out_res: (Set[K], Bool)) { op == searchOp() ? - c_in == c_out && res == (k in c_in) : + ((c_in, (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)) + ((c_in ++ {| k |}, (k !in c_in))) : + ((c_in -- {| k |}, (k in c_in)))) } } @@ -89,7 +89,7 @@ interface NodeImpl { 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 ==> 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) @@ -173,63 +173,62 @@ interface GiveUpTemplate[Node: NodeImpl, LockF: Lock] { own(r.authSet, AuthSetRef.frag(SetRefRA.set_constr({|n|})) ) } - pred cssR(r: Ref, c: Set[K], g_i: Flow_K, lockval: Map[Ref, Int]) { + pred cssR(r: Ref, c: Set[K], g_i: Flow_K) { (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) + (exists l: Ref, b: Bool :: + own(n.lock, l, 1.0) && L.is_lock(l, (r, n), b))) + && 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) + exists g_i: Flow_K :: + cssR(r, c, g_i) } - lemma cssInFp(r: Ref, n:Ref, c: Set[K], g_i: Flow_K, lockval: Map[Ref, Int]) - requires cssR(r, c, g_i, lockval) + lemma cssInFp(r: Ref, n:Ref, c: Set[K], g_i: Flow_K) + requires cssR(r, c, g_i) requires inFP(r, n) ensures n in g_i.dom - ensures cssR(r, c, g_i, lockval) + ensures cssR(r, c, g_i) ensures inFP(r, n) { - unfold cssR(r, c, g_i, lockval); + unfold cssR(r, c, g_i); 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); + fold cssR(r, c, g_i); } - lemma fpInCss(r: Ref, n:Ref, c: Set[K], g_i: Flow_K, lockval: Map[Ref, Int]) - requires cssR(r, c, g_i, lockval) + lemma fpInCss(r: Ref, n:Ref, c: Set[K], g_i: Flow_K) + requires cssR(r, c, g_i) requires n in g_i.dom ensures inFP(r, n) - ensures cssR(r, c, g_i, lockval) + ensures cssR(r, c, g_i) { - unfold cssR(r, c, g_i, lockval); + unfold cssR(r, c, g_i); 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); + fold cssR(r, c, g_i); } - 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) + lemma root_fp(r: Ref, c: Set[K], g_i: Flow_K) + requires cssR(r, c, g_i) + ensures cssR(r, c, g_i) ensures r in g_i.dom { - unfold cssR(r, c, g_i, lockval); + unfold cssR(r, c, g_i); 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); + fold cssR(r, c, g_i); } } \ No newline at end of file diff --git a/test/concurrent/templates/give-up-simplified.rav b/test/concurrent/templates/give-up-simplified.rav new file mode 100644 index 0000000..7678609 --- /dev/null +++ b/test/concurrent/templates/give-up-simplified.rav @@ -0,0 +1,549 @@ +include "./flows_ra.rav" +include "./ccm_instances.rav" +include "./keyset_ra.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 } + + func opSpec(op: Op, k: K, c_in: Set[K]) returns (c_out_res: (Set[K], Bool)) { + op == searchOp() ? + ((c_in, (k in c_in))) : + (op == insertOp() ? + ((c_in ++ {| k |}, (k !in c_in))) : + ((c_in -- {| k |}, (k in c_in)))) + } +} + +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], flow_int: 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 :: {outset(i,n)} 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, implicit ghost c1: Set[K], implicit ghost c2: Set[K], implicit ghost i_n1: Flow_K, implicit ghost 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]) + + 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 cc: Set[K]) + requires k in keyspace + atomic requires css(r, c) + atomic ensures css(r, cc) && opSpec(dop, k, c) == ((cc, res)) +} + + +interface GiveUpTemplate[Node: NodeImpl] { + 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 + field lock: Bool + + func globalinv(g_i: Flow_K, r: Ref) returns (res: Bool) + { + 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(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) { + globalRes(r, c, g_i) && + (forall n: Ref :: n in g_i.dom ==> + (exists b: Bool, cn: Set[K], intfn: Flow_K :: + own(n.lock, b, 1.0) && (b ? true : nodePred(r, n, cn, intfn)))) + } + + pred css(r: Ref; c: Set[K]) { + exists g_i: Flow_K :: cssR(r, c, g_i) + } + + proc lockNode(n: Ref, implicit ghost b: Bool) + atomic requires own(n.lock, b, 1.0) + atomic ensures own(n.lock, true, 1.0) && b == false + + proc unlockNode(n: Ref) + atomic requires own(n.lock, true, 1.0) + atomic ensures own(n.lock, false, 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) && nodePred(r, n, c_n, i_n) && inFP(r, n) + { + ghost var phi: AtomicToken := bindAU(); + + ghost var g_i0: Flow_K; + + ghost val c0: Set[K] := openAU(phi); + unfold css(r, c0); + cssInFp(r, n, c0); + + unfold cssR(r); + + lockNode(n); + c_n, i_n :| nodePred(r, n, c_n, i_n); + fold cssR(r, c0); + fold css(r, c0); + + commitAU(phi, c_n, i_n); + } + + proc unlockNodeHigh(r: Ref, n: Ref, ghost c_n: Set[K], ghost i_n: Flow_K, implicit ghost c: Set[K]) + requires inFP(r, n) + requires 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 val c1: Set[K] := openAU(phi); + unfold css(r, c1); + cssInFp(r, n, c1); + + unfold cssR(r, c1); + + {! + ghost var b: Bool; + b :| own(n.lock, b, 1.0); + if (!b) { + unfold nodePred(r, n, c_n, i_n); + unfold nodePred(r, n, c_n, i_n); + Node.nodeSepStar(n); + } + !} + + unlockNode(n); + fold cssR(r, c1, g_i1); + assert cssR(r, c1, g_i1); + fold css(r, c1); + + commitAU(phi); + } + + + lemma cssInFp(r: Ref, n:Ref, c: Set[K], implicit ghost g_i: Flow_K) + requires cssR(r, c, g_i) + requires inFP(r, n) + ensures n in g_i.dom + ensures cssR(r, c, g_i) + ensures inFP(r, n) + { + unfold cssR(r, c, g_i); + 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); + } + + + lemma fpInCss(r: Ref, n:Ref, c: Set[K], implicit ghost g_i: Flow_K) + requires cssR(r, c, g_i) + requires n in g_i.dom + ensures inFP(r, n) + ensures cssR(r, c, g_i) + { + unfold cssR(r, c, g_i); + 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); + } + + lemma root_fp(r: Ref, c: Set[K], implicit ghost g_i: Flow_K) + requires cssR(r, c, g_i) + ensures cssR(r, c, g_i) + ensures r in g_i.dom + { + unfold cssR(r, c, g_i); + unfold globalRes(r, c, g_i); + + fold globalRes(r, c, g_i); + fold cssR(r, c, g_i); + } + + 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:false + ); + + fold nodePred(r, r, {||}, i_r); + + fold globalRes(r, {||}, i_r); + fold cssR(r, {||}, i_r); + assert cssR(r, {||}, i_r); + fold css(r, {||}); + } + + lemma fpInStep(r: Ref, n: Ref, n1: Ref, k: K, c: Set[K], c_n: Set[K], i_n: Flow_K, implicit ghost g_i: Flow_K) + requires cssR(r, c, g_i) + requires nodePred(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) + ensures nodePred(r, n, c_n, i_n) + ensures n1 in g_i.dom + { + if (n1 !in g_i.dom) { + unfold cssR(r, c, g_i); + unfold nodePred(r, n, c_n, i_n); + + unfold globalRes(r, c, g_i); + + ghost var i_o: Flow_K = Flow_K.frame(g_i, i_n); + + assert i_o.out[n1] == Multiset_K.frame(g_i.out[n1], i_n.out[n1]); + assert k !in outset(g_i, n1); + + fold nodePred(r, n, c_n, i_n); + fold globalRes(r, c, g_i); + fold cssR(r, c, g_i); + } + } + + proc traverse(r: Ref, n: Ref, k: K, implicit ghost c: Set[K]) + returns (nn: Ref, ghost cnn: Set[K], ghost i_nn: Flow_K) + requires inFP(r, n) + atomic requires css(r, c) + atomic ensures css(r, c) + ensures nodePred(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 nodePred(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 nodePred(r, n, c_n, i_n); + + if (succ) { + + ghost val c1: Set[K] := openAU(phi); + unfold css(r, c1); + + cssInFp(r, n, c1); + fpInStep(r, n, n1, k, c1, c_n, i_n); + fpInCss(r, n1, c1); + + 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 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 val c1: Set[K] := openAU(phi); + + unfold css(r, c1); + + unfold cssR(r, c1); + unfold globalRes(r, c1); + + fold globalRes(r, c1); + fold cssR(r, c1); + + fpInCss(r, r, c1); + + 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 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))) + { + if (dop == searchOp || !res) { + c1 := c; + } else { + if (dop == insertOp) { + c1 := c ++ {| k |}; + } else { + c1 := c -- {| k |}; + } + + 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 val c0: Set[K] := openAU(phi); + unfold css(r, c0); + + root_fp(r, c0); + fpInCss(r, r, c0); + 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 nodePred(r, n, c_n, i_n); + + succ, res, c_n1 := Node.decisiveOp(dop, n, k, c_n, i_n); + if (succ) { + + ghost val c1: Set[K] := openAU(phi); + unfold css(r, c1); + cssInFp(r, n, c1); + unfold cssR(r, c1); + + {! + ghost var b: Bool; + b :| own(n.lock, b, 1.0); + if (!b) { + unfold nodePred(r, n, c_n1, i_n); + Node.nodeSepStar(n); + } + !} + + unlockNode(n); + + unfold globalRes(r, c1); + cc := keyset_theorem(r, dop, k, c_n, c_n1, c1, res, keyset(i_n)); + fold globalRes(r, cc); + + fold nodePred(r, n, c_n1, i_n); + fold cssR(r, cc); + 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