From 4bb7220e6fff0dbcebecba90d82112539b61a00b Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Sun, 3 Jun 2018 22:04:43 +0200
Subject: [PATCH] fix build
---
_CoqProject | 3 ---
theories/lang/lock.v | 8 +++++---
2 files changed, 5 insertions(+), 6 deletions(-)
diff --git a/_CoqProject b/_CoqProject
index c03b2e2b..bd1908a6 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -63,9 +63,6 @@ theories/typing/lib/refcell/ref_code.v
theories/typing/lib/refcell/refmut_code.v
theories/typing/lib/refcell/refmut.v
theories/typing/lib/refcell/ref.v
-theories/typing/lib/rwlock/rwlock.v
-theories/typing/lib/rwlock/rwlockreadguard.v
-theories/typing/lib/rwlock/rwlockwriteguard.v
theories/typing/examples/get_x.v
theories/typing/examples/rebor.v
theories/typing/examples/unbox.v
diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index 7fea4090..15f6c449 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -7,7 +7,9 @@ Set Default Proof Using "Type".
Definition mklock_unlocked : val := λ: ["l"], "l" <- #false.
Definition mklock_locked : val := λ: ["l"], "l" <- #true.
-Definition try_acquire : val := λ: ["l"], CAS "l" #false #true AcqRel Relaxed.
+(* If the CAS fails, it's a relaxed-read.
+ If the CAS succeeds, it's a acq-read and relaxed-write *)
+Definition try_acquire : val := λ: ["l"], CAS "l" #false #true Relaxed AcqRel Relaxed.
Definition acquire : val :=
rec: "acquire" ["l"] := if: try_acquire ["l"] then #☠ else "acquire" ["l"].
Definition release : val := λ: ["l"], "l" <-ʳᵉˡ #false.
@@ -135,9 +137,9 @@ Section proof.
wp_rec. iMod ("Hproto" with "HP") as (γ R0 Vb) "(#[Eq lc] & inv & Hclose)".
iDestruct "lc" as (?) "lc".
iMod (rel_True_intro True%I tid with "[//]") as "rTrue".
- iApply (GPS_PPRaw_CAS_simple (lock_interp R0) _ _ _ _
+ iApply (GPS_PPRaw_CAS_int_simple (lock_interp R0) _ _ _ _ _
(Z_of_bool false) #true () (λ _, R0)%I (λ _ _, True)%I
- with "[$lc $inv rTrue]"); [done|by right|by left|..].
+ with "[$lc $inv rTrue]");[done|by left|done|by right|by left|..].
{ iSplitL ""; [|iSplitL ""]; [iNext; iModIntro..|].
- iIntros (?? _). by iApply lock_interp_comparable.
- by iIntros (??)"_ #$".
--
GitLab