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

ICFP21 artifact: more detailed comment on the pipeline

parent 0593a2b0
......@@ -30,9 +30,9 @@ Section pipeline.
Context (capacity : nat) (capacity_min : capacity 1).
(*
ICFP21: Here is a simple client code that makes uses of the data structure
ICFP21: Here is a simple client code that makes use of the data structure
defined in bounded_queue.v. It corresponds to the code listings in Figure 11
of the paper.
of the paper (except that functions `pipef` and `pipeg` have been inlined).
*)
Definition pipeline : val := λ: "f" "g" "xs",
......@@ -87,6 +87,8 @@ Section Spec.
pipeline_proto is what the paper calls PipeInvInner.
f_thread is what the paper calls PipeF.
g_thread is what the paper calls PipeG.
cur_f is what the paper calls n<sub>f</sub>.
cur_g is what the paper calls n<sub>g</sub>.
*)
Definition pipeline_proto f g R xs γqueue γcur_f γcur_g : iProp Σ := (
......
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