diff --git a/semantics.opam b/semantics.opam
index e6b9f5bce81a9f633dd6852b13dfa4deafa1264b..90fbb39e32d712bf1e654889da87abff7d434af3 100644
--- a/semantics.opam
+++ b/semantics.opam
@@ -9,10 +9,9 @@ bug-reports: "https://gitlab.mpi-sws.org/FP/semantics-course/issues"
version: "dev"
depends: [
- "coq" { (>= "8.13" & < "8.16~") | (= "dev") }
- "coq-iris" { (= "dev.2022-08-14.0.25e3b14e") | (= "dev") }
- "coq-iris-heap-lang" { (= "dev.2022-08-14.0.25e3b14e") | (= "dev") }
- "coq-equations" { (= "1.2.4+8.13") | (= "1.3+8.14") | (= "1.3+8.15") }
+ "coq" { (>= "8.13" & < "8.17~") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2022-09-21.1.291dc89e") | (= "dev") }
+ "coq-equations" { (= "1.2.4+8.13") | (= "1.3+8.14") | (= "1.3+8.15") | (= "1.3+8.16") }
"coq-autosubst" { = "1.7" }
]
diff --git a/theories/program_logics/concurrency.v b/theories/program_logics/concurrency.v
index 92b43192003801c7b72d7e2762ae4fb0fc3788e1..435a83470d44e08b73c0b7144550ab2d56944841 100644
--- a/theories/program_logics/concurrency.v
+++ b/theories/program_logics/concurrency.v
@@ -1,5 +1,6 @@
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import lang notation.
+From iris.bi Require Import fractional.
From iris.base_logic Require Import invariants.
From iris.heap_lang Require Export primitive_laws proofmode.
From iris.algebra Require Import excl auth numbers.
@@ -41,7 +42,6 @@ Global Notation "{{ P } } e {{ v , Q } }" := (□ (P%I -∗ WP e {{ v, Q%I }}))%
Definition assert (e : expr) : expr :=
if: e then #() else #0 #0.
-
Section cas.
Context `{heapGS Σ}.
@@ -225,14 +225,13 @@ Definition with_lock' e1 e2 := (with_lock (e1: expr) (λ: <>, e2)%E).
Section with_lock.
Context `{heapGS Σ}.
- (* TODO: exercise *)
Lemma with_lock_spec Φ (l c : val) P :
is_lock l P -∗
(P -∗ WP c #() {{ v, P ∗ Φ v }}) -∗
WP with_lock l c {{ Φ }}.
Proof.
- (* FIXME exercise for you *)
- Admitted.
+ (* FIXME: exercise *)
+ Admitted.
End with_lock.
(** Exclusive Ghost Token *)
@@ -263,8 +262,9 @@ End lock_lemmas.
Section excl_spin_lock.
Context `{heapGS Σ} `{lockG Σ}.
- Definition is_excl_lock v (γ : gname) P : iProp Σ :=
- is_lock v P. (* FIXME *)
+ Definition is_excl_lock v γ P :=
+ is_lock v P
+ .
Instance is_excl_lock_pers v γ P : Persistent (is_excl_lock v γ P).
Proof. apply _. Qed.
@@ -272,28 +272,29 @@ Section excl_spin_lock.
Lemma newlock_spec' P :
⊢ {{ P }} newlock #() {{ v, ∃ γ, is_excl_lock v γ P }}.
Proof.
- (* FIXME *)
+ (* FIXME: exercise *)
Admitted.
Lemma acquire_spec' v γ P :
⊢ {{ is_excl_lock v γ P }} acquire v {{ w, ⌜w = #()⌝ ∗ locked γ ∗ P }}.
Proof.
- (* FIXME *)
+ (* FIXME: exercise *)
Admitted.
Lemma release_spec' v γ P :
⊢ {{ is_excl_lock v γ P ∗ locked γ ∗ P }} release v {{ w, True }}.
Proof.
- (* FIXME *)
+ (* FIXME: exercise *)
Admitted.
Lemma really_exclusive v γ P :
⊢ {{ is_excl_lock v γ P ∗ locked γ }} assert (!v = #true) {{ _, True }}.
Proof.
- (* FIXME *)
+ (* FIXME: exercise *)
Admitted.
End excl_spin_lock.
+
(** Parallel composition *)
Definition await : val :=
rec: "await" "x" :=
@@ -316,7 +317,7 @@ Section para_comp.
WP e2 #() {{ _, Q2 }} -∗
WP comp e1 e2 {{ _, Q1 ∗ Q2 }}.
Proof using Type*.
- (* FIXME *)
+ (* FIXME: exercise *)
Admitted.
End para_comp.
@@ -332,6 +333,7 @@ Definition parallel_counter : expr :=
Section counter.
Context `{heapGS Σ} `{lockG Σ} `{ghost_varG Σ nat}.
+
(** You may find the GhostVariable algebra useful.
Iris already provides it, and you can use the following lemmas.
*)
@@ -339,20 +341,17 @@ Section counter.
(*Check ghost_var_agree.*)
(*Check ghost_var_update.*)
(* Note: Iris supports splitting a ghost variable into halves via the usual destruct patterns.
- For example:
- *)
+ For example: *)
Lemma gvar_split_halves γ (a : nat) :
ghost_var γ 1 a -∗ ghost_var γ (1/2) a ∗ ghost_var γ (1/2) a.
Proof.
iIntros "[H1 H2]". iFrame.
Qed.
- (* TODO exercise *)
- (* TODO put hint about ghost_var here *)
Lemma parallel_counter_spec :
⊢ {{ True }} parallel_counter {{ v, ⌜v = #2⌝ }}.
Proof using Type*.
- (* FIXME *)
+ (* FIXME: exercise *)
Admitted.
End counter.
@@ -364,19 +363,19 @@ Definition acquire_mutex : val :=
Section mutex.
Context `{heapGS Σ}.
- (* TODO this is an exercise *)
Notation "l '↦:' P" := (∃ v : val, l ↦ v ∗ P v)%I (at level 40) : stdpp_scope.
Definition is_mutex (v : val) (P : val → iProp Σ) : iProp Σ :=
- True (* FIXME *).
+ True
+ .
Instance is_mutex_pers v P : Persistent (is_mutex v P).
Proof. apply _. Qed.
Lemma mkmutex_spec P (v : val) :
⊢ {{ P v }} mkmutex v {{ v, is_mutex v P }}.
Proof.
- (* FIXME *)
+ (* FIXME: exercise *)
Admitted.
Lemma acquire_mutex_spec P (v : val) :
@@ -384,7 +383,7 @@ Section mutex.
acquire_mutex v
{{ w, ∃ (l : loc) (rl : val), ⌜w = (#l, rl)%V⌝ ∗ l ↦: P ∗ {{ l ↦: P }} rl #() {{ _, True }} }}.
Proof.
- (* FIXME *)
+ (* FIXME: exercise *)
Admitted.
End mutex.
@@ -510,12 +509,12 @@ Section channel_spec.
Lemma send_spec v d :
⊢ {{ is_channel v ∗ Pc d }} send v d {{ v, ⌜v = #()⌝ }}.
Proof using Pers.
- (* FIXME *)
+ (* FIXME: exercise *)
Admitted.
Lemma receive_spec v :
⊢ {{ is_channel v }} receive v {{ d, Pc d }}.
Proof using Pers.
- (* FIXME *)
+ (* FIXME: exercise *)
Admitted.
End channel_spec.
diff --git a/theories/program_logics/reloc/proofmode.v b/theories/program_logics/reloc/proofmode.v
index 92fe38cbb62e02aa6dec1329a71e848842ff665f..2bfc11f4cdcf28b228adc276238d8076c6fb6511 100644
--- a/theories/program_logics/reloc/proofmode.v
+++ b/theories/program_logics/reloc/proofmode.v
@@ -72,7 +72,7 @@ Lemma src_expr_step_pure `{relocGS Σ} (ϕ : Prop) n e1 e2 K E :
src_expr (fill K e1) ={E}=∗ src_expr (fill K e2).
Proof.
iIntros (Hphi Hpure ?) "(#CTX & Hs)".
- iFrame "CTX". by iApply src_step_pures.
+ iFrame "CTX". iApply src_step_pures; [ | done..]; done.
Qed.
Lemma tac_src_pure `{relocGS Σ} e K' e1 e2 Δ1 E1 i1 e' ϕ ψ Q n :