diff --git a/theories/examples/bounded_queue.v b/theories/examples/bounded_queue.v
index 41b4228a709c67ff10b6cc58810ed37d873b1bd0..70d20ebce22cef71c0c96c7ef02e68b6719dc050 100644
--- a/theories/examples/bounded_queue.v
+++ b/theories/examples/bounded_queue.v
@@ -31,7 +31,7 @@ Axiom modulo_spec : ∀ `{cosmoG Σ} (n m : Z),
(*
ICFP21: Below follows the implementation, in our toy deep-embedded language,
- of the bounded queue with a circular buffer. It corresponds to Figure 5 of
+ of the bounded queue with a circular buffer. It corresponds to Figure 8 of
the paper. “capacity” is a non-zero integer constant.
It is worth noting that the toy language is untyped. This code, in particular,
@@ -215,7 +215,7 @@ Section Spec.
Notation Zlength ls := (Z.of_nat (length ls)) (only parsing).
(* ICFP21: This is the definition of the ghost state representing slot tokens
- (Section 4.5 of the paper).
+ (Section 4.5 and Figure 9d of the paper).
Whereas the paper uses finite maps over Z, here we model them using lists.
There isn’t really a technical advantage in doing so, to be honest, and it
requires careful shifting so that no negative index is involved. *)
@@ -270,6 +270,9 @@ Section Spec.
- rewrite insert_app_r_alt // Nat.sub_diag //=.
Qed.
+ (* ICFP21: The lemmas below correspond to properties of the tokens. They are
+ more specific than the properties shown in Figure 10c of the paper. *)
+
Lemma own_token_list_read γtoks t h xVs i :
0 ≤ t →
-capacity ≤ i →
@@ -408,7 +411,7 @@ Section Spec.
(*
ICFP21: Here is the internal invariant of the bounded queue as described in
- Figure 6 of the paper (“queue_proto” being called “QueueInvInner” in the
+ Figure 9e of the paper (“queue_proto” being called “QueueInvInner” in the
paper).
Vt and Vh are the head and tail views, respectively (denoted by calligraphic
@@ -486,7 +489,7 @@ Section Spec.
Proof. by apply _. Qed.
(* ICFP21: this is the predicate “IsQueue” from the paper, which exposes the
- public state of the queue. *)
+ public state of the queue (Figure 9a of the paper). *)
Definition is_queue γ Vt Vh xVs : iProp Σ := (
own γ (◯E (Vt, Vh, xVs))
)%I.
@@ -576,7 +579,7 @@ Section Spec.
}
Qed.
- (* ICFP21: this is the spec of “make“, as presented in Figure 3 of the paper,
+ (* ICFP21: this is the spec of “make“, as presented in Figure 5 of the paper,
along with its proof for this particular implementation (recall that
“monPred_in V” is what is denoted by ↑V in the paper; ⎡P⎤ is the embedding
of an objective assertion P (of type iProp) into general Cosmo assertions
@@ -653,7 +656,7 @@ Section Spec.
iFrame "Hγ◯". repeat (iExists _). by iFrame "I".
Qed.
- (* ICFP21: this is the spec of “try_enqueue“, as presented in Figure 3 of the
+ (* ICFP21: this is the spec of “try_enqueue“, as presented in Figure 5 of the
paper, along with its proof.
<<< ∀ x, P >>> e <<< Q, RET v >>> is the notation for a logically atomic
triple (P,e,Q) with a binder x and returning value v.
@@ -942,7 +945,7 @@ Section Spec.
wp_pures. by iApply "HΦ".
Qed.
- (* ICFP21: this is the spec of “try_dequeue“, as presented in Figure 3 of the
+ (* ICFP21: this is the spec of “try_dequeue“, as presented in Figure 5 of the
paper, along with its proof. Same remarks as with “try_enqueue”. *)
Lemma try_dequeue_spec (E : coPset) q γ V :
E ## ↑queueN →
@@ -1238,7 +1241,7 @@ Section Spec.
wp_pures. iApply "HΦ".
Qed.
- (* ICFP21: this is the spec of “enqueue“, as presented in Figure 3 of the
+ (* ICFP21: this is the spec of “enqueue“, as presented in Figure 5 of the
paper, along with its proof (which is a direct induction by using the
specification of “try_enqueue“ in a modular fashion). *)
Lemma enqueue_spec (E : coPset) q γ x V :
@@ -1258,7 +1261,7 @@ Section Spec.
- iIntros "Hq". iLeft. iFrame. iIntros "!> AU !>". wp_pures. by iApply "IH".
Qed.
- (* ICFP21: this is the spec of “dequeue“, as presented in Figure 3 of the
+ (* ICFP21: this is the spec of “dequeue“, as presented in Figure 5 of the
paper, along with its proof (which is a direct induction by using the
specification of “try_dequeue“ in a modular fashion). *)
Lemma dequeue_spec (E : coPset) q γ V :
diff --git a/theories/examples/pipeline.v b/theories/examples/pipeline.v
index d714cd71b71a792229bf6d27c8aa3a1750542936..2886e06720ea510d14efa6571da4258e1d808e57 100644
--- a/theories/examples/pipeline.v
+++ b/theories/examples/pipeline.v
@@ -31,7 +31,7 @@ Context (capacity : nat) (capacity_min : capacity ≥ 1).
(*
ICFP21: Here is a simple client code that makes uses of the data structure
- defined in bounded_queue.v. It corresponds to the code listings in Figure 7
+ defined in bounded_queue.v. It corresponds to the code listings in Figure 11
of the paper.
*)
@@ -82,7 +82,7 @@ Section Spec.
(*
ICFP21: Here is the internal invariant of the pipeline, as described in
- Figure 9 of the paper.
+ Figure 13 of the paper.
“pipeline_proto” is what the paper calls “PipeInvInner”.
“f_thread” is what the paper calls “PipeF”.
@@ -117,7 +117,7 @@ Section Spec.
)%I.
(*
- ICFP21: Here is the spec of the pipeline, as shown in Figure 8 of the paper,
+ ICFP21: Here is the spec of the pipeline, as shown in Figure 12 of the paper,
along with its proof.
*)
diff --git a/theories/program_logic/atomic.v b/theories/program_logic/atomic.v
index 3dc90a6696ca8e32a5e8495c666ab7dded7580bc..4123500715f91c8dad4ff029f0a760ff8866fc32 100644
--- a/theories/program_logic/atomic.v
+++ b/theories/program_logic/atomic.v
@@ -17,10 +17,10 @@ Set Default Proof Using "Type".
Ralf Jung et al. “Iris: monoids and invariants as an orthogonal basis for
concurrent reasoning”. POPL, 2015. http://plv.mpi-sws.org/iris/paper.pdf
+ (Section 7)
Ralf Jung. “Logical Atomicity in Iris: the Good, the Bad, and the Ugly”.
Iris Workshop, 2019. https://people.mpi-sws.org/~jung/iris/talk-iris2019.pdf
- (Section 7)
<<< ∀ x, P >>> e <<< ∃ y, Q, RET v >>> denotes the logically atomic triple
with a binder x (which is bound in P, Q, v), precondition P, expression e,