Commit 2773194c authored by Jonas Kastberg's avatar Jonas Kastberg

Added more differences between paper and mechanisation to README

parent a34d13a6
Pipeline #21574 passed with stage
in 17 minutes and 36 seconds
...@@ -23,11 +23,15 @@ correspond to the following parts of the paper: ...@@ -23,11 +23,15 @@ correspond to the following parts of the paper:
- [theories/channel/channel.v](theories/channel/channel.v): The definitional - [theories/channel/channel.v](theories/channel/channel.v): The definitional
semantics of bidirectional channels in terms of Iris's HeapLang language. semantics of bidirectional channels in terms of Iris's HeapLang language.
- [theories/channel/proto_model.v](theories/channel/proto_model.v): The CPS - [theories/channel/proto_model.v](theories/channel/proto_model.v): The CPS
model of Dependent Separation Protocols. model of Dependent Separation Protocols over arbitrary BI-logics.
- [theories/channel/proto_channel.v](theories/channel/proto_channel.v): The - [theories/channel/proto_channel.v](theories/channel/proto_channel.v): The
definition of the connective `↣` for channel ownership, and lemmas instantiation of protocols with the Iris logic, definition of the connective `↣`
corresponding to the Actris proof rules. The relevant proof rules are as for channel endpoint ownership, and lemmas corresponding to the Actris proof rules.
follows: The relevant definitions and proof rules are as follows:
+ `iProto Σ`: The type of protocols.
+ `iProto_message`: The constructor for sends and receives.
+ `iProto_end`: The constructor for terminated protocols.
+ `mapsto_proto`: endpoint ownership `↣`.
+ `new_chan_proto_spec`: proof rule for `new_chan`. + `new_chan_proto_spec`: proof rule for `new_chan`.
+ `send_proto_spec` and `send_proto_spec_packed`: proof rules for `send`, the + `send_proto_spec` and `send_proto_spec_packed`: proof rules for `send`, the
first version is more convenient to use in Coq, but otherwise the same as first version is more convenient to use in Coq, but otherwise the same as
...@@ -38,6 +42,31 @@ correspond to the following parts of the paper: ...@@ -38,6 +42,31 @@ correspond to the following parts of the paper:
+ `select_spec`: proof rule for `select`. + `select_spec`: proof rule for `select`.
+ `branch_spec`: proof rule for `branch`. + `branch_spec`: proof rule for `branch`.
## Notation
The notation for Dependent Separation Protocols differ between the
mechanisation and the paper.
The paper uses the following notation:
- Send: ! x_1 .. x_n < v > { P } . prot
- Recv: ? x_1 .. x_n < v > { P } . prot
- End: end
- Select: prot_1 {Q_1} ⊕ {Q_2} prot_2
- Branch: prot_1 {Q_1} & {Q_2} prot_2
- Append: prot_1 · prot_2
- Dual: An overlined protocol
The mechanisation uses the following notation:
- Send: <!> x_1 .. x_n, MSG v {{ P }} ; prot
- Recv: <?> x_1 .. x_n, MSG v {{ P }} ; prot
- End: END
- Select: prot_1 <{Q_1} + {Q_2}> prot_2
- Branch: prot_1 <{Q_1} & {Q_2}> prot_2
- Append: prot_1 <++> prot_2
- Dual: Nothing
## Weakest preconditions and Coq tactics ## Weakest preconditions and Coq tactics
The presentation of Actris logic in the paper makes use of Hoare triples. In The presentation of Actris logic in the paper makes use of Hoare triples. In
...@@ -126,10 +155,14 @@ mechanization in Coq: ...@@ -126,10 +155,14 @@ mechanization in Coq:
There are a number of small differences between the paper presentation There are a number of small differences between the paper presentation
of Actris and the formalization in Coq, that are briefly discussed here. of Actris and the formalization in Coq, that are briefly discussed here.
- **Notation**
See the section "Notation" above.
- **Weakest preconditions versus Hoare triples** - **Weakest preconditions versus Hoare triples**
See the section "Weakest preconditions and Coq tactics" above. See the section "Weakest preconditions and Coq tactics" above.
- **Connectives for physical ownership of channels** - **Connectives for physical ownership of channels**
In the paper, physical ownership of a channel is formalized using a single In the paper, physical ownership of a channel is formalized using a single
......
...@@ -26,8 +26,8 @@ Futhermore, we define the following operations: ...@@ -26,8 +26,8 @@ Futhermore, we define the following operations:
- [iProto_dual], which turns all [Send] of a protocol into [Recv] and vice-versa - [iProto_dual], which turns all [Send] of a protocol into [Recv] and vice-versa
- [iProto_app], which appends two protocols as described in proto_model.v - [iProto_app], which appends two protocols as described in proto_model.v
An encoding of the usual branching connectives [prot1 {Q1}<+>{Q2} prot2] and An encoding of the usual branching connectives [prot1 <{Q1}+{Q2}> prot2] and
[prot1 {Q1}<&>{Q2} prot2], inspired by session types, is also included in this [prot1 <{Q1}&{Q2}> prot2], inspired by session types, is also included in this
file. file.
The logical connective for protocol ownership is denoted as [c ↣ prot]. It The logical connective for protocol ownership is denoted as [c ↣ prot]. It
......
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