From 745fd15f972030522d565f34db2a3d53361faa68 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 31 Aug 2023 12:44:23 +0200
Subject: [PATCH] update dependencies
---
coq-reloc.opam | 2 +-
theories/examples/ticket_lock.v | 5 +++--
theories/experimental/hocap/ticket_lock.v | 3 ++-
3 files changed, 6 insertions(+), 4 deletions(-)
diff --git a/coq-reloc.opam b/coq-reloc.opam
index 7cb4689..b708dc8 100644
--- a/coq-reloc.opam
+++ b/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" }
]
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 4d57628..c81377b 100644
--- a/theories/examples/ticket_lock.v
+++ b/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.
diff --git a/theories/experimental/hocap/ticket_lock.v b/theories/experimental/hocap/ticket_lock.v
index d0f33f9..22f1f1a 100644
--- a/theories/experimental/hocap/ticket_lock.v
+++ b/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.
--
GitLab