Commit d60bcda9 authored by Glen Mével's avatar Glen Mével
Browse files

ICFP21 artifact: fix figure numbers

parent d191abb9
......@@ -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 isnt 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 :
......
......@@ -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.
*)
......
......@@ -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,
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment