update dependencies

coq-reloc.opam

@@ -6,7 +6,7 @@ bug-reports: "https://gitlab.mpi-sws.org/dfrumin/reloc/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/dfrumin/reloc.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2023-06-14.0.f0e415b6") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-08-29.5.af0a091b") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 

theories/examples/ticket_lock.v

@@ -8,7 +8,8 @@ From iris.heap_lang.lib Require Export ticket_lock.
 (* A different `acquire` funciton to showcase the atomic rule for FG_increment *)
 Definition acquire : val := λ: "lk",
   let: "n" := FG_increment (Snd "lk") in
-  wait_loop "n" "lk".
+  (* breaking the ticket-lock abstraction... *)
+  ticket_lock.wait_loop "n" "lk".
 (* A different `release` function to showcase the rule for wkincr *)
 Definition release : val := λ: "lk", wkincr (Fst "lk").
 
@@ -128,7 +129,7 @@ Section refinement.
   Lemma wait_loop_refinement (lo ln : loc) γ lk (m : nat) :
     inv N (lockInv lo ln γ lk) -∗
     ticket γ m -∗
-    REL wait_loop #m (#lo, #ln)%V << reloc.lib.lock.acquire lk : ().
+    REL ticket_lock.wait_loop #m (#lo, #ln)%V << reloc.lib.lock.acquire lk : ().
   Proof.
     iIntros "#Hinv Hticket".
     rel_rec_l.

theories/experimental/hocap/ticket_lock.v

@@ -37,7 +37,8 @@ Section refinement.
     Cnt (N.@"cnt1") cn γln -∗
     Cnt (N.@"cnt2") co γlo -∗
     ticket γ m -∗
-    REL wait_loop #m (co, cn)%V << spin_lock.acquire l' : ().
+    (* breaking the ticket_lock abstraction... *)
+    REL ticket_lock.wait_loop #m (co, cn)%V << spin_lock.acquire l' : ().
   Proof.
     iIntros "#Hinv #Hcntn #Hcnto Hticket".
     iLöb as "IH". rel_rec_l.