Commit 56a4744f authored by jihgfee's avatar jihgfee

Added descriptive headers to all files

parent 42ba5b0a
(** This file contains the definition of the Channel language encoding,
being a pair of buffers, with the three message-passing primitives
[new_chan], [send] and [receive], along with their respective specifications.
The abstract representation of a channel endpoint is two buffer references
and a lock. [new_chan] creates references to two empty buffers and a lock, and
returns a pair of such endpoints, where the order of the two references
determines the polarity of the endpoints.
The [send] primitive takes such an endpoint abstraction and adds an element to
the first buffer under the lock. Conversely [recv] loops until there is
something in the second, locking during each peek.
The specifications are defined in terms of the logical connectives [is_chan]
and [chan_own], which respectively determines the contents of a channel and
the ownership of it.
*)
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import excl auth list.
......@@ -9,6 +27,7 @@ Instance side_inhabited : Inhabited side := populate Left.
Definition side_elim {A} (s : side) (l r : A) : A :=
match s with Left => l | Right => r end.
(** Message-Passing Primitives *)
Definition new_chan : val :=
λ: <>,
let: "l" := lnil #() in
......@@ -39,6 +58,7 @@ Definition recv : val :=
| NONE => "go" "c"
end.
(** Channel ghost functor *)
Class chanG Σ := {
chanG_lockG :> lockG Σ;
chanG_authG :> auth_exclG (listO valO) Σ;
......@@ -65,6 +85,7 @@ Section channel.
chan_r_name : gname
}.
(** The invariant of channels *)
Definition chan_inv (γ : chan_name) (l r : loc) : iProp Σ :=
( ls rs,
llist sbi_internal_eq l ls own (chan_l_name γ) ( to_auth_excl ls)
......@@ -79,6 +100,18 @@ Section channel.
Global Instance is_chan_persistent : Persistent (is_chan γ c1 c2).
Proof. by apply _. Qed.
Lemma chan_inv_alt s γ l r :
chan_inv γ l r ⊣⊢ ls rs,
llist sbi_internal_eq (side_elim s l r) ls
own (side_elim s chan_l_name chan_r_name γ) ( to_auth_excl ls)
llist sbi_internal_eq (side_elim s r l) rs
own (side_elim s chan_r_name chan_l_name γ) ( to_auth_excl rs).
Proof.
destruct s; rewrite /chan_inv //=.
iSplit; iDestruct 1 as (ls rs) "(?&?&?&?)"; iExists rs, ls; iFrame.
Qed.
(** The ownership of channels *)
Definition chan_own (γ : chan_name) (s : side) (vs : list val) : iProp Σ :=
own (side_elim s chan_l_name chan_r_name γ) ( to_auth_excl vs)%I.
......@@ -94,9 +127,9 @@ Section channel.
wp_lam.
wp_apply (lnil_spec with "[//]"); iIntros (l) "Hl".
wp_apply (lnil_spec with "[//]"); iIntros (r) "Hr".
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl []))) as (lsγ) "[Hls Hls']".
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl []))) as (lsγ) "[Hls Hls']".
{ by apply auth_both_valid. }
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
{ by apply auth_both_valid. }
wp_apply (newlock_spec N ( ls rs,
llist sbi_internal_eq l ls own lsγ ( to_auth_excl ls)
......@@ -107,17 +140,6 @@ Section channel.
rewrite /chan_inv /=. eauto 20 with iFrame.
Qed.
Lemma chan_inv_alt s γ l r :
chan_inv γ l r ⊣⊢ ls rs,
llist sbi_internal_eq (side_elim s l r) ls
own (side_elim s chan_l_name chan_r_name γ) ( to_auth_excl ls)
llist sbi_internal_eq (side_elim s r l) rs
own (side_elim s chan_r_name chan_l_name γ) ( to_auth_excl rs).
Proof.
destruct s; rewrite /chan_inv //=.
iSplit; iDestruct 1 as (ls rs) "(?&?&?&?)"; iExists rs, ls; iFrame.
Qed.
Lemma send_spec Φ E γ c1 c2 v s :
is_chan γ c1 c2 -
(|={,E}=> vs,
......@@ -194,4 +216,5 @@ Section channel.
iIntros "!> !>" (v vs' ->) "Hvs".
iMod ("HΦ" with "[//] Hvs") as "HΦ". iIntros "!> !> !>". by wp_pures.
Qed.
End channel.
(** This file contains tactics for the message-passing
connectives, as well as the necessary typeclasses.
This includes a way of reducing protocols to a normal
form, to prepare them for use in the appropriate
specifications. This normalisation includes e.g.
resolving duals.
*)
From iris.heap_lang Require Export proofmode notation.
From iris.proofmode Require Export tactics.
From actris Require Export proto_channel.
......
(** This file contains the instantiation of the
Dependent Separation Protocols with the encoded messages.
For starters this means fixing the types of message to the
language value type [val] and the logic to the iris logic [iProp Σ].
It then defines a convenient way of constructing instances of the type
via [iProto_end] and [iProto_message] with associated notation,
as well as type-specific variants of [dual] and [append].
An encoding of branching behaviour is additionally included, defined
in terms of sending and receiving boolean flags, along with relevant notation.
The logical connectives of protocol ownership [c >-> prot] are then defined.
This is achieved through Iris invariants and ghost state along with the
logical connectives of the channel encodings.
Lastly, relevant typeclasses are defined for each of the above notions,
such as contractiveness and non-expansiveness, after which the specifications
of the message-passing primitives are defined in terms of the protocol connectives.
*)
From actris.channel Require Export channel.
From actris.channel Require Import proto_model.
From iris.base_logic.lib Require Import invariants.
......
(** This file defines the model of Dependent Separation Protocols,
along with various operations on the connective, such as append
and map.
Dependent Separation Protocols can ultimately be expressed as:
proto := 1 + (B * (V -> (▶ proto -> PROP) -> PROP))
Here the left-hand side of the sum is the terminal protocol
[proto_end], while the right-hand side is [proto_message],
where B is the canonical representation of actions determining
whether the protocol sends or receives, and
(V -> (▶ proto -> PROP) -> PROP) is a continuation that
depends on a communicated value V and the dependent tail
(▶ proto -> PROP) from protocols guarded under laters,
to the propositions of the logic.
The type is defined as a solution to a recursive domain
equation, as it is self-referential under the guard of ▶.
*)
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import cofe_solver.
......
(** This file includes basic examples that each
encapsulate a feature of the Dependent Separation Protocols.
*)
From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation lib.spin_lock.
From actris.utils Require Import contribution.
(** Basic *)
Definition prog1 : val := λ: <>,
let: "c" := start_chan (λ: "c'", send "c'" #42) in
recv "c".
(** References *)
Definition prog2 : val := λ: <>,
let: "c" := start_chan (λ: "c'", send "c'" (ref #42)) in
! (recv "c").
(** Delegation *)
Definition prog3 : val := λ: <>,
let: "c1" := start_chan (λ: "c1'",
let: "cc2" := new_chan #() in
......@@ -17,12 +23,14 @@ Definition prog3 : val := λ: <>,
send (Snd "cc2") #42) in
recv (recv "c1").
(** Dependent Behaviour *)
Definition prog4 : val := λ: <>,
let: "c" := start_chan (λ: "c'",
let: "x" := recv "c'" in send "c'" ("x" + #2)) in
send "c" #40;;
recv "c".
(** Higher-Order *)
Definition prog5 : val := λ: <>,
let: "c" := start_chan (λ: "c'",
let: "f" := recv "c'" in send "c'" (λ: <>, "f" #() + #2)) in
......@@ -30,6 +38,7 @@ Definition prog5 : val := λ: <>,
send "c" (λ: <>, !"r");;
recv "c" #().
(** Locks *)
Definition prog_lock : val := λ: <>,
let: "c" := start_chan (λ: "c'",
let: "l" := newlock #() in
......@@ -40,6 +49,7 @@ Definition prog_lock : val := λ: <>,
Section proofs.
Context `{heapG Σ, proto_chanG Σ}.
(** Protocols for their respective programs *)
Definition prot1 : iProto Σ :=
(<?> MSG #42; END)%proto.
......@@ -65,6 +75,7 @@ Fixpoint prot_lock (n : nat) : iProto Σ :=
| S n' => <?> MSG #21; prot_lock n'
end%proto.
(** Specs and proofs of their respective programs *)
Lemma prog1_spec : {{{ True }}} prog1 #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
......
(** This file implements a distributed map service,
a specification thereof and its proofs. *)
From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation lib.spin_lock.
From actris.utils Require Import llist contribution.
......
(** This file implements a map-reduce program,
a specification thereof and its proofs. *)
From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation.
From actris.utils Require Import llist compare contribution group.
......
(** This file implements a distributed Merge Sort,
a specification thereof and its proofs. *)
From stdpp Require Import sorting.
From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation.
......
(** This file implements a looping distributed Merge Sort,
a specification thereof and its proofs. *)
From stdpp Require Import sorting.
From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation.
......
(** This file implements a fine-grained Merge Sort,
a specification thereof and its proofs. *)
From stdpp Require Export sorting.
From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation.
......
(** This file provides utility for defining and using
the commonly used ghost functor over authoritative exclusive ownership. *)
From iris.proofmode Require Import tactics.
From iris.algebra Require Import excl auth.
From iris.base_logic.lib Require Import own.
......
(** This file includes a definition and specification
for comparing values based on a given interpretation [I]
and a relation [R], along with an implementation in the [heap_lang]
language, given the [≤] relation.*)
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
......
(** This file defines a ghost functor for tracking
"contributions" made to a shared concurrent effort.
It is ultimately defined as:
contribution := Auth (Option ((Pos * A) + Excl 1))
Intuitively it allows one to allocate a [server] and
a number of [client] fragments. The server keeps track
of the number of active clients, and what resources they
are currently holding.
To deallocate a client it must hold no resources.
To deallocate a server there must be no remaining clients.
*)
From iris.base_logic Require Export base_logic lib.iprop lib.own.
From iris.proofmode Require Export tactics.
From iris.algebra Require Import excl auth csum gmultiset frac_auth.
......
(** This file provides utility for grouping elements
based on keys. *)
From stdpp Require Export prelude.
From Coq Require Export SetoidPermutation.
......
(** This file defines an encoding of lists in the [heap_lang]
language, along with common functions such as append and split. *)
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import assert.
......
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