From 15a1c8011eff36a3299701e38419f3c999f3f2ad Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Fri, 5 Apr 2024 02:00:14 +0200
Subject: [PATCH] Misc changes
---
multi_actris/channel/channel.v | 44 +++++++-----------
multi_actris/channel/proofmode.v | 1 -
multi_actris/channel/proto.v | 50 ++-------------------
multi_actris/channel/proto_model.v | 5 ++-
multi_actris/examples/basics.v | 2 -
multi_actris/examples/leader_election_del.v | 1 -
multi_actris/utils/matrix.v | 3 --
7 files changed, 22 insertions(+), 84 deletions(-)
diff --git a/multi_actris/channel/channel.v b/multi_actris/channel/channel.v
index 7e68d81..9fa9113 100644
--- a/multi_actris/channel/channel.v
+++ b/multi_actris/channel/channel.v
@@ -1,23 +1,20 @@
-(** This file contains the definition of the channels, encoded as a pair of
-lock-protected buffers, and their primitive proof rules. Moreover:
+(** This file contains the definition of the channels,
+and their primitive proof rules. Moreover:
- It defines the connective [c ↣ prot] for ownership of channel endpoints,
which describes that channel endpoint [c] adheres to protocol [prot].
-- It proves Actris's specifications of [send] and [recv] w.r.t. dependent
- separation protocols.
-
-An encoding of the usual (binary) choice connectives [prot1 <{Q1}+{Q2}> prot2]
-and [prot1 <{Q1}&{Q2}> prot2], inspired by session types, is also included in
-this file.
+- It proves Actris's specifications of [send] and [recv] w.r.t.
+ multiparty dependent separation protocols.
In this file we define the three message-passing connectives:
-- [new_chan] creates references to two empty buffers and a lock, and returns a
- pair of endpoints, where the order of the two references determines the
- polarity of the endpoints.
-- [send] takes an endpoint and adds an element to the first buffer.
-- [recv] performs a busy loop until there is something in the second buffer,
- which it pops and returns, locking during each peek.
+- [new_chan] creates an n*n matrix of references where [i,j] is the singleton
+ buffer from participant i to participant j
+- [send] takes an endpoint, a participant id, and a value, and puts the value in
+ the reference corresponding to the participant id, and waits until recv takes
+ it out.
+- [recv] takes an endpoint, and a participant id, and waits until a value is put
+ into the corresponding reference.
It is additionaly shown that the channel ownership [c ↣ prot] is closed under
the subprotocol relation [⊑] *)
@@ -50,7 +47,6 @@ Definition send : val :=
let: "l" := matrix_get "m" "i" "j" in
"l" <- SOME "v";; wait "l".
-(* TODO: Move recursion further in *)
Definition recv : val :=
rec: "go" "c" "j" :=
let: "m" := Fst "c" in
@@ -185,23 +181,15 @@ Section channel.
(λ i j l, ∃ γt,
inv (nroot.@"p") (chan_inv γ (γEs !!! i) γt i j
l))%I); [done..| |].
- { iApply (big_sepL_intro).
- iIntros "!>" (k tt Hin).
- iApply (big_sepL_intro).
- iIntros "!>" (k' tt' Hin').
- iIntros (l) "Hl".
+ { iApply (big_sepL_intro). iIntros "!>" (k tt Hin). iApply (big_sepL_intro).
+ iIntros "!>" (k' tt' Hin'). iIntros (l) "Hl".
iMod (own_alloc (Excl ())) as (γ') "Hγ'"; [done|].
- iExists γ'.
- iApply inv_alloc.
- iNext.
- iLeft. iFrame. }
- iIntros (mat) "Hmat".
- iApply "HΦ".
+ iExists γ'. iApply inv_alloc. iNext. iLeft. iFrame. }
+ iIntros (mat) "Hmat". iApply "HΦ".
iExists _, _, _. iFrame "#∗".
rewrite left_id. iSplit; [done|].
iApply (big_sepL_impl with "H").
- iIntros "!>" (i ? HSome') "(Hauth & Hfrag & Hown)".
- iFrame.
+ iIntros "!>" (i ? HSome') "(Hauth & Hfrag & Hown)". iFrame.
rewrite (list_lookup_total_alt ps).
simpl. rewrite right_id_L. rewrite HSome'. iFrame.
Qed.
diff --git a/multi_actris/channel/proofmode.v b/multi_actris/channel/proofmode.v
index 5f9d7b8..81ca7e6 100644
--- a/multi_actris/channel/proofmode.v
+++ b/multi_actris/channel/proofmode.v
@@ -338,7 +338,6 @@ Proof.
iNext. iRewrite -"Hp1". done.
Qed.
-(* TODO: Improve automation *)
Tactic Notation "iProto_consistent_take_step_step" :=
let i := fresh in
let j := fresh in
diff --git a/multi_actris/channel/proto.v b/multi_actris/channel/proto.v
index fdd225f..75efec7 100644
--- a/multi_actris/channel/proto.v
+++ b/multi_actris/channel/proto.v
@@ -1,50 +1,6 @@
-(** This file defines the core of the Actris logic: It defines dependent
-separation protocols and the various operations on it like dual, append, and
-branching.
-
-Dependent separation protocols [iProto] are defined by instantiating the
-parameterized version in [proto_model] with the type of propositions [iProp] of Iris.
-We define ways of constructing instances of the instantiated type via two
-constructors:
-- [iProto_end], which is identical to [proto_end].
-- [iProto_message], which takes an [action] and an [iMsg]. The type [iMsg] is a
- sequence of binders [iMsg_exist], terminated by the payload constructed with
- [iMsg_base] based on arguments [v], [P] and [prot], which are the value, the
- carried proposition and the [iProto] tail, respectively.
-
-For convenience sake, we provide the following notations:
-- [END], which is simply [iProto_end].
-- [∃ x, m], which is [iMsg_exist] with argument [m].
-- [MSG v {{ P }}; prot], which is [iMsg_Base] with arguments [v], [P] and [prot].
-- [<a> m], which is [iProto_message] with arguments [a] and [m].
-
-We also include custom notation to more easily construct complete constructions:
-- [<a x1 .. xn> m], which is [<a> ∃ x1, .. ∃ xn, m].
-- [<a x1 .. xn> MSG v; {{ P }}; prot], which constructs a full protocol.
-
-Futhermore, we define the following operations:
-- [iProto_dual], which turns all [Send] of a protocol into [Recv] and vice-versa.
-- [iProto_app], which appends two protocols.
-
-In addition we define the subprotocol relation [iProto_le] [⊑], which generalises
-the following inductive definition for asynchronous subtyping on session types:
-
- p1 <: p2 p1 <: p2 p1 <: !B.p3 ?A.p3 <: p2
----------- ---------------- ---------------- ----------------------------
-end <: end !A.p1 <: !A.p2 ?A.p1 <: ?A.p2 ?A.p1 <: !B.p2
-
-Example:
-
-!R <: !R ?Q <: ?Q ?Q <: ?Q
-------------------- --------------
-?Q.!R <: !R.?Q ?P.?Q <: ?P.?Q
-------------------------------------
- ?P.?Q.!R <: !R.?P.?Q
-
-Lastly, relevant type classes instances 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. *)
+(** This file defines the core of the Multiparty Actris logic:
+It defines multiparty dependent separation protocols, and the Multiparty Actris
+ghost theory. *)
From iris.algebra Require Import gmap excl_auth gmap_view.
From iris.proofmode Require Import proofmode.
From iris.base_logic Require Export lib.iprop.
diff --git a/multi_actris/channel/proto_model.v b/multi_actris/channel/proto_model.v
index 8bd4bd3..007f8ef 100644
--- a/multi_actris/channel/proto_model.v
+++ b/multi_actris/channel/proto_model.v
@@ -12,8 +12,9 @@ recursive domain equation:
Here, the left-hand side of the sum is used for the terminated process, while
the right-hand side is used for the communication constructors. The type
-[action] is an inductively defined datatype with two constructors [Send] and
-[Recv]. Compared to having an additional sum in [proto], this makes it
+[action] is a pair of a an inductively defined datatype [tag] with two
+constructors [Send] and [Recv], and a synchronosation id of [nat].
+Compared to having an additional sum in [proto], this makes it
possible to factorize the code in a better way.
The remainder [V → ▶ proto → PROP] is a predicate that ranges over the
diff --git a/multi_actris/examples/basics.v b/multi_actris/examples/basics.v
index 82a0173..80169be 100644
--- a/multi_actris/examples/basics.v
+++ b/multi_actris/examples/basics.v
@@ -37,7 +37,6 @@ Section channel.
⊢ iProto_consistent iProto_roundtrip.
Proof. rewrite /iProto_roundtrip. iProto_consistent_take_steps. Qed.
- (* TODO: Fix nat/Z coercion. *)
Lemma roundtrip_prog_spec :
{{{ True }}} roundtrip_prog #() {{{ RET #42 ; True }}}.
Proof using chanG0 heapGS0 Σ.
@@ -320,7 +319,6 @@ Section forwarder.
(<(Recv, 1) @ (x:Z)> MSG #x ;
<(Send, 0)> MSG #x ; END)%proto].
- (* TODO: Anonymous variable in this is unsatisfactory *)
Lemma iProto_forwarder_consistent :
⊢ iProto_consistent iProto_forwarder.
Proof.
diff --git a/multi_actris/examples/leader_election_del.v b/multi_actris/examples/leader_election_del.v
index 7c40b66..1ff5abd 100644
--- a/multi_actris/examples/leader_election_del.v
+++ b/multi_actris/examples/leader_election_del.v
@@ -179,7 +179,6 @@ Section ring_leader_election_example.
(relay_recv_aux i (relay_recv_prot i)).
Proof. apply (fixpoint_unfold (relay_recv_aux i)). Qed.
-
Definition prot_pool : list (iProto Σ) :=
[rle_preprot 3 0 1 (λ id_max, forward_prot (relay_send_prot id_max) 3 0 1 id_max);
rle_prot 0 1 2 (λ id_max, forward_prot (relay_send_prot id_max) 0 1 2 id_max) false;
diff --git a/multi_actris/utils/matrix.v b/multi_actris/utils/matrix.v
index 066da4f..166b7d2 100644
--- a/multi_actris/utils/matrix.v
+++ b/multi_actris/utils/matrix.v
@@ -24,7 +24,6 @@ Section with_Σ.
[∗ list] j ↦ _ ∈ replicate n (),
P i j (l +â‚— pos n i j).
-
Lemma array_to_matrix_pre l n m v :
l ↦∗ replicate (n * m) v -∗
[∗ list] i ↦ _ ∈ replicate n (), (l +ₗ i*m) ↦∗ replicate m v.
@@ -42,7 +41,6 @@ Section with_Σ.
by iFrame.
Qed.
- (* TODO: rename *)
Lemma big_sepL_replicate_type {A B} n (x1 : A) (x2 : B) (P : nat → iProp Σ) :
([∗ list] i ↦ _ ∈ replicate n x1, P i) ⊢
([∗ list] i ↦ _ ∈ replicate n x2, P i).
@@ -117,7 +115,6 @@ Section with_Σ.
{ iIntros "!>" (k x HIn).
iApply (big_sepL_lookup_acc _ _ j ()).
by apply lookup_replicate. }
- simpl.
rewrite {1}(big_sepL_lookup_acc _ (replicate m ()) i ());
[|by apply lookup_replicate].
iDestruct "Hm" as "[[Hij Hi] Hm]".
--
GitLab