Add personal scratch work

So far, just some notes on failing CLH lock and lock-coupled list verifications.

test/lucas-noob-work/clh_lock.rav

@@ -0,0 +1,116 @@
+// REF: https://dada.cs.washington.edu/research/tr/1993/02/UW-CSE-93-02-02.pdf
+// REF: diaframe_heap_lang_examples/comparison/clh_lock.v (MPI-SWS gitlab)
+
+module CLHRequest {
+  field state: Bool; // Whether request is PENDING (true) or GRANTED (false)
+  field watch: Ref;  // Pointer to predecessor in queue --- we wait on its state
+
+  pred request_rep(r: Ref, b: Bool)
+  {
+    exists predreq: Ref :: own(r, watch, predreq, 1.0) && own(r, state, b, 1.0)
+      // TODO: Is this enough? Can we get additional assurance that predreq
+      // points to a valid CLHRequest? I guess we could recursively call
+      // request_rep here on predreq, but not sure if this supported in Raven.
+  }
+
+  // NOTE: Seems like is_request would just be redundant with request_rep here.
+  // I can't think of a reason right now to have a separate is_request predicate
+  // here (like with locks) --- locks have an additional resource field that
+  // they're protecting, which is why having an additional predicate makes
+  // sense, but requests here don't have the same structure.
+  // pred is_request() {}
+
+  proc create()
+    returns (req: Ref)
+    ensures request_rep(req, false)
+  {
+    req := new (state: false, watch: null);
+    fold request_rep(req, false);
+  }
+}
+
+interface CLHLock {
+  module R: Library.Type
+  module Agree = Library.Agree[R]
+
+  ghost field agr: Agree
+
+  // Resource protected by the lock
+  pred resource(r: R)
+
+  field tail: Ref; // Pointer to latest (tail) request in queue
+                   // (or: request to be watched by next requester)
+
+  pred lock_rep(l: Ref; b: Bool)
+  {
+    // What do we do with b: Bool here? I think the policy is basically: if the
+    // lock's request is GRANTED/false, the lock is unlocked. Otherwise, it is
+    // locked some other process and possibly has other competing acquisition
+    // requests in the queue.
+    exists req: Ref ::
+      own(l, tail, req, 1.0) &&
+      CLHRequest.request_rep(req, b)
+  }
+
+  // NOTE: Ripped directly from the lock.rav higher-order module for locks.
+  pred is_lock(l: Ref; r: R, b: Bool) {
+    own(l, agr, Agree.agree(r))
+    && lock_rep(l, b)
+    && (b ? true : resource(r))
+  }
+
+  // According to Craig, need to allocate a Request (node in Diaframe) for the lock
+  // and mark the Request as GRANTED (i.e. the lock is free). In Diaframe, the
+  // state field is false/true vs. GRANTED/PENDING in Craig's paper.
+  // It actually seems that in Diaframe, we combine the lock and the lock node
+  // initialization, i.e. why the allocation looks like ref (ref #false).
+  proc create(r: R)
+    returns (lk: Ref)
+    requires resource(r)
+    ensures is_lock(lk, false)
+  {
+    // NOTE: This won't work --- procedure calls are only allowed as top-level
+    // statements (for simplicity). We can't nest them inside an allocation.
+    // This should be fixed now, but previously we had:
+    // new (tail: CLHRequest.create(), agr: Agree.agree(r))
+    // NOTE: Agree.agree(r) is fine because agree, I think, is a *function*,
+    // i.e. it has no side-effects.
+    var lkreq: Ref := CLHRequest.create();
+    lk := new (tail: lkreq, agr: Agree.agree(r));
+  }
+
+  // acquire takes two arguments: a Ref to the lock and a Ref to a node that is
+  // associated with the acquiring process.
+  // acquire needs to set its own node's (aka request in Craig's parlance)
+  // "locked" ("state" in Craig's parlance) to True. Then it needs to perform
+  // an (atomic) fetch-and-store that replaces the lock's tail with a pointer
+  // to the acquiring node and the acquiring node's watching field with the lock's
+  // current tail.
+  proc acquire(lk: Ref, req: Ref)
+    requires is_lock(lk) && request_rep(req)
+  {
+    req.state := true;
+    // TODO: The "fetch-and-store" here needs to be atomic --- I think?
+    // NOTE: This won't work! Only 1 logically atomic step per statement. This
+    // is 2 steps: a read and a write. Should be fixed below, but it was
+    // originally:
+    // req.watch := lk.tail
+    currtail := lk.tail;
+    req.watch := currtail;
+    lk.tail := req;
+  }
+
+  // release takes one argument: a Ref to the node that is associated with the
+  // releasing process. It returns a Ref that represents the Request/node
+  // granted to it by its predecessor --- this is now the Request/node that the
+  // current process owns.
+  // TODO: How do we ensure that only the process holding the lock can release it?
+  proc release(req: Ref)
+    returns (predreq: Ref)
+    requires request_rep(req, false)
+    ensures request_rep(predreq)
+  {
+    req.state := false;
+    predreq := req.watch;
+  }
+}

test/lucas-noob-work/clh_lock.v

@@ -0,0 +1,106 @@
+(* This is material copied from the Diaframe proof of the CLH lock. I add some
+annotations here that help tie it to the canonical description of the lock in
+Craig's paper "Bulding FIFO and Priority-Queuing Spin Locks from Atomic Swap". *)
+
+From diaframe.heap_lang Require Import proof_automation wp_auto_lob.
+From diaframe.lib Require Import own_hints.
+From iris.algebra Require Import agree frac excl.
+
+Definition new_lock : val :=
+  λ: "_", ref (ref #false).
+
+Definition new_node : val :=
+  λ: "_",
+    let: "ret" := AllocN #2 NONE in (* NOTE: Nodes in Diaframe, it seems, are tuples --- hence, the AllocN #2. We set both fields here to NONE, then we set the first field to false in the following line. It helps to notice that we are directly referencing memory locations here --- not logical structures at the programming language level ---  so when we set the value at "ret" to be ref #false, we are setting the first memory unit (doesn't really matter, but i.e. would be a byte in a byte-addressable system), or the first field (logically speaking), to false. The second field remains NONE. *)
+    "ret" <- ref #false;;
+    "ret".
+
+Definition wait_on : val := (* NOTE: This is the spin part of the spinlock. *)
+  rec: "wait_on" "l" :=
+    if: ! "l" then
+      "wait_on" "l"
+    else
+      #().
+
+Definition acquire : val :=
+  λ: "lk" "node",
+    let: "l" := ! "node" in
+    "l" <- #true;;
+    let: "pred" := Xchg "lk" "l" in  (* also called fetch_and_store sometimes *)
+    ("node" +ₗ #1) <- "pred";; (* NOTE: Here, we are setting our Request/node state to PENDING (true in Diaframe code). Then, we set the lock's tail (lk) to the pointer to the acquiring Request/node's reference and the acquiring Request/node's predecessor pointer (i.e. the pointer we're watching to determine our place in line) to the lock's tail (the one from before we swapped it out/set it to something else). *)
+    wait_on "pred".
+
+Definition release : val :=
+  λ: "node",
+    ! "node" <- #false;; (* NOTE: false == GRANTED and true == PENDING in Craig's paper. We can interpret false here as false to the statement "waiting to acquire" or "is pending". *)
+    "node" <- ! ("node" +ₗ #1). (* NOTE: this step corresponds to the step in Craig's description of grant_lock where the releaser takes ownership of the Request/node granted to it by its predecessor --- in the Diaframe code here, ("node" + #1) is the second field in the node tuple that stores the pointer to the predecessor reference (see line 30 above for the associated operation in acquire) *)
+
+(* NOTE: I guess in this implementation, each calling thread must keep track of its own associated node/Request that it currently owns. It's returned by release though, for example, so it can be reused as long as we save that returned value. *)
+
+(* NOTE: Below, we have the specifications and proofs of the implementation above. *)
+
+Definition clh_lockR := prodR (agreeR $ leibnizO loc) fracR.
+Class clh_lockG Σ := CLHLockG {
+  #[local] clh_lock_tokG :: inG Σ clh_lockR;
+  #[local] clh_lock_exclG :: inG Σ $ exclR unitO
+}.
+Definition clh_lockΣ : gFunctors := #[GFunctor clh_lockR; GFunctor $ exclR unitO].
+
+#[local] Obligation Tactic := program_verify.
+Global Program Instance subG_clh_lockΣ {Σ} : subG clh_lockΣ Σ → clh_lockG Σ.
+
+Section spec.
+  Context `{!heapGS Σ, clh_lockG Σ}.
+
+  Let N := nroot .@ "clhlock".
+  Definition N_node := N .@ "node".
+
+  Definition queued_loc γe l γ R : iProp Σ :=
+    own γ (to_agree l, 1%Qp) ∨ (∃ (b : bool), l ↦{#1/2} #b ∗ (⌜b = true⌝ ∨ (⌜b = false⌝ ∗ R ∗ own γe (Excl ()) ∗ own γ (to_agree l, 1/2)%Qp ∗ l ↦{#1/2} #b))).
+  (* NOTE: Lemma for a queued location? Not sure what the arguments here mean. Either gamma owns 1.0 of l. Or there is some boolean b s.t. the value at l is b and we own 1/2 of l. Either b is true, which should mean the location is attempting to acquire the lock (?) or b is false (we hold the lock) AND we own resource R, we have exclusive ownership of γe, which I guess is the watched node, l owns 1/2 of γ, which I guess is the owned node, and l also owns half of the state bool of the owned node? *)
+  (* NOTE: From the spin_lock.v example, it seems like gamma and gammae should indicate ghost state, particularly a ghost name. How does this make sense here? In spin_lock.v, own gamma (Excl ()) indicates locked gamma, which means that the lock is currently locked/held (as the name suggests lol). In fact, queued_loc looks *a lot* like lock_inv in the spin lock verification --- I believe it serves the same purpose. BTW: each node's first field is a bool for its state and its second field is a pointer to the node it's watching. l should be that first field, i.e. the bool for the state. R is the resource and indicates whether the process that owns the node currently has access to that resource. γe is the ghost name representing the lock itself. γ is the ghost name representing the node itself (the one that's queued). *)
+  (* NOTE: I gotta figure out what the left disjoint here means. The right disjoint makes more sense given our deduced interpretation above. When a process queues a location/node, it has 1/2 ownership over it (the points to just means that the first field of the node is the state boolean). If b is true, i.e. we are still pending/in the process of acquiring the lock, that's the whole spec --- the predecessor node's process holds the other 1/2 ownership over our node. If b is false, i.e. we now have the lock, we own R, we have exclusive lock access (own gammae (Excl ())), we also own the other 1/2 of our current node now (since there's no more predecessor node). The question remains: what is the own gammae (to_agree l, ...) stuff doing, both in the left disjunct and in the right disjunct in the b = false branch. *)
+  (* NOTE: Also, for this lock, shouldn't we be watching the predecessor's state? The above interpretation makes it seem like we're just looking at our own node's state. *)
+
+  Definition free_node n : iProp Σ :=
+    ∃ (l : loc) v, n ↦ #l ∗ (n +ₗ 1) ↦ v ∗ l ↦ #false.
+  (* NOTE: l is a location, not sure what v is. n is the node. The first field of the node points to the address of a location l that holds the state value. The second field of the node points to some v...this would generally be the watched node, but it doesn't seem to matter here. the value at l should be false, since this is the default value when a node is first created. *)
+  (* NOTE: Being free is the opposite of being queued (i.e. this predicate should be the converse of queued_loc above). *)
+
+  Definition acquired_node γe n R : iProp Σ :=
+    ∃ (l p : loc), n ↦ #l ∗ (∃ γ, inv N_node (queued_loc γe l γ R) ∗ own γ (to_agree l, 1/2)%Qp) ∗ l ↦{#1/2} #true ∗
+                  (n +ₗ 1) ↦ #p ∗ p ↦ #false ∗ own γe (Excl ()).
+  (* NOTE: l and p are both locations. p is the predecessor. n needs to be queued (can't be free?). Like above, first field of n points to address of state location.  *)
+
+  Definition lock_inv γe lk R : iProp Σ :=
+    ∃ (l : loc), lk ↦ #l ∗ ∃ γ, own γ (to_agree l, 1/2)%Qp ∗ inv N_node (queued_loc γe l γ R).
+  (* NOTE: Lock points to the address of location l. There is some gamma, a ghost name representing a node, that we own 1/2 of and that has value l (note that lk points to the address of l, which would also then be the address of this node). I think thinking through and relating lock_inv to the definition of queued_loc will help me understand what the own γ (to_agree l, 1/2)%Qp stuff is doing. Specifically, the own here makes it so that we cannot take the left disjunct of queued_loc...*)
+  (* NOTE: BTW, the fact that we have γe here strongly supports the fact that it is a ghost name representing the lock itself. *)
+
+  Definition is_lock γe R v : iProp Σ :=
+    ∃ (lk : loc), ⌜v = #lk⌝ ∗ inv N (lock_inv γe lk R).
+
+  (* These are the specifications for each of the procedure definitions at the top of this file. They are just Hoare triples, using the lemmas we defined just above this. *)
+  Global Program Instance new_lock_spec :
+    SPEC {{ True }}
+      new_lock #()
+    {{ (lk : val), RET lk; (∀ R, R ={⊤}=∗ ∃ γe, is_lock γe R lk) }}.
+
+  Global Program Instance new_node_spec :
+    SPEC {{ True }}
+      new_node #()
+    {{ (n : loc), RET #n; free_node n }}.
+
+  Global Program Instance acquire_spec R (n : loc) (lk : val) γe :
+    SPEC {{ is_lock γe R lk ∗ free_node n }}
+      acquire lk #n
+    {{ RET #(); R ∗ acquired_node γe n R }}.
+
+  Global Program Instance release_spec R (n : loc) γe :
+    SPEC {{ R ∗ acquired_node γe n R }}
+      release #n
+    {{ RET #(); free_node n }}.
+
+  Definition acquired_mutual_exclusion γe n m R : acquired_node γe n R ∗ acquired_node γe m R ⊢ False
+    := verify. (* Cannot do Lemma _ : _ := verify unfortunately. If proper reuse is wanted this should be a Mergable instance *)
+End spec.

test/lucas-noob-work/clh_lock_clean.rav

@@ -0,0 +1,170 @@
+// REF: https://dada.cs.washington.edu/research/tr/1993/02/UW-CSE-93-02-02.pdf
+// REF: diaframe_heap_lang_examples/comparison/clh_lock.v (MPI-SWS gitlab)
+
+interface CLHLock {
+  module R: Library.Type
+  module Agree = Library.Agree[R]
+  module BoolType : Library.Type {
+    rep type T = Bool
+  }
+  module FracBool = Library.Frac[BoolType]
+
+  import FracBool.frac_chunk
+  ghost field agr: Agree
+
+  // ===========================================================================
+  // Section defining loc (just a flag for storing node "locked" state)
+  // ===========================================================================
+  field locked: Bool;
+  field l_agr: Bool; // QUESTION: How do I use a unit type? Seems like it's
+  // been deprecated for an empty tuple, but how do I define a tuple type? For
+  // now, I guess I'll just have a bool that's always set to true.
+
+  // ===========================================================================
+  // Section defining node fields, predicates, and procedures
+  // ===========================================================================
+  field loc: Ref;
+  field predecessor: Ref;
+
+  pred free_node(node: Ref) {
+    exists ln: Ref, pn: Ref ::
+      own(node, loc, ln, 1.0) &&
+      own(ln, locked, false, 1.0) &&
+      own(node, predecessor, pn, 1.0) &&
+      own(ln, l_agr, true, 1.0)
+  }
+
+  proc create_node()
+    returns (node: Ref)
+    ensures free_node(node)
+  {
+    var newloc: Ref;
+    newloc := new (locked: false, l_agr: true);
+    node := new (loc: newloc, predecessor: null);
+    // NOTE: Might need to be false
+    fold free_node(node) [b_disj := true];
+  }
+
+  // ===========================================================================
+  // Lock definition
+  // ===========================================================================
+  // Resource protected by the lock
+  pred resource(r: R)
+
+  // Structurally, the lock is a pointer to the tail loc in our implicit queue
+  field tail: Ref
+
+  // ===========================================================================
+  // Predicates and invariants used for verification
+  // ===========================================================================
+  inv queued_loc(l: Ref, r: R) {
+    exists b_disj: Bool, b: Bool ::
+      (b_disj ? own(l, l_agr, true, 1.0) : own(l, locked, b, 0.5) &&
+      (!b ==> resource(r) && own(l, l_agr, true, 0.5) && own(l, locked, b, 0.5)))
+  }
+
+  inv lock_inv(lk: Ref, r: R) {
+    exists l: Ref ::
+      own(lk, tail, l, 1.0) &&
+      own(l, l_agr, true, 0.5) &&
+      queued_loc(l, r)
+  }
+
+  pred acquired_node(node: Ref, r: R) {
+    exists ln: Ref, pn: Ref ::
+      own(node, loc, ln, 1.0) &&
+      queued_loc(ln, r) && own(ln, l_agr, true, 0.5) &&
+      own(ln, locked, true, 0.5) &&
+      own(node, predecessor, pn, 1.0) &&
+      own(pn, locked, false, 0.5) &&
+      resource(r)
+  }
+
+  // ===========================================================================
+  // Actual procedures (with specifications) on locks
+  // ===========================================================================
+  proc create_lock(r: R)
+    returns (lk: Ref)
+    requires resource(r)
+    ensures lock_inv(lk, r)
+  {
+    var l: Ref;
+    l := new (locked: false, l_agr: true);
+    lk := new (tail: l, agr: Agree.agree(r));
+    fold queued_loc(l, r) [b_disj := false];
+    fold lock_inv(lk, r);
+  }
+
+  proc wait_on(lk: Ref, pn: Ref, ln: Ref, node: Ref, implicit ghost r: R)
+    requires lock_inv(lk, r) && queued_loc(ln, r) &&
+    own(node, loc, ln, 1.0) &&
+    own(node, predecessor, pn, 1.0) &&
+    own(ln, l_agr, true, 0.5) &&
+    own(ln, locked, true, 0.5) &&
+    queued_loc(pn, r) && own(pn, l_agr, true, 0.5)
+    ensures acquired_node(node, r)
+  {
+    ghost var branch: Bool;
+    unfold queued_loc(pn, r) {branch :| b_disj};
+    var b: Bool := pn.locked;
+    // assert (!b ==> resource(r) && own(pn, l_agr, true, 0.5) &&
+    // own(pn, locked, b, 0.5));
+
+    {!
+      if (!b) {
+        // TODO: think this through a bit more
+        fold acquired_node(node, r);
+        // NOTE: This line currently causes crash...won't dig further for now.
+        // fpu(pn, full_agr, frac_chunk(false, 1.0), frac_chunk(true, 1.0));
+        assert ln != pn;
+        // assert own(pn, full_agr, false, 1.0);
+        assert own(pn, locked, b, 0.5);
+        fold queued_loc(pn, r) [b := b, b_disj := true];
+      } else {
+        fold queued_loc(pn, r) [b := b, b_disj := branch];
+        // TODO: Updates to ghost fields in ghost blocks are not allowed (when
+        // wrapped in a Frac) -- message Ekansh about this
+      }
+    !}
+
+    if (b) {
+      wait_on(lk, pn, ln, node, r);
+    }
+  }
+
+  proc xchg(lk: Ref, ln: Ref, implicit ghost t: Ref)
+    returns (pn: Ref)
+    atomic requires own(lk, tail, t, 1.0)
+    atomic ensures own(lk, tail, ln, 1.0) && pn == t
+
+  proc acquire(lk: Ref, node: Ref, implicit ghost r: R)
+    requires lock_inv(lk, r) && free_node(node)
+    ensures acquired_node(node, r)
+  {
+    unfold free_node(node);
+    var ln: Ref := node.loc;
+    ln.locked := true;
+
+    unfold lock_inv(lk, r);
+    var pn: Ref := xchg(lk, ln);
+    fold queued_loc(ln, r) [b_disj := false];
+    fold lock_inv(lk, r);
+
+    // Set new predecessor
+    node.predecessor := pn;
+    // Wait on the predecessor
+    wait_on(lk, pn, ln, node, r);
+  }
+
+  proc release(node: Ref, implicit ghost r: R)
+    requires acquired_node(node, r)
+    ensures free_node(node)
+  {
+    unfold acquired_node(node, r);
+    var ln: Ref := node.loc;
+    ln.locked := false;
+    var pn: Ref := node.predecessor;
+    node.loc := pn;
+    fold free_node(node);
+  }
+}