Actris merge requestshttps://gitlab.rts.mpi-sws.org/iris/actris/-/merge_requests2021-07-18T15:33:41Zhttps://gitlab.rts.mpi-sws.org/iris/actris/-/merge_requests/25WIP: Interpretation of πDILL2021-07-18T15:33:41ZDan FruminWIP: Interpretation of πDILLHi, I would like to request comments on something that I've been working on.
πDILL is a type system based on intuitionistic linear logic, formulated in the dual context-style: https://doi.org/10.1017/S0960129514000218
In this PR I trie...Hi, I would like to request comments on something that I've been working on.
πDILL is a type system based on intuitionistic linear logic, formulated in the dual context-style: https://doi.org/10.1017/S0960129514000218
In this PR I tried to write down the interpretation for this system using `heap_lang` (instead of pi-calculus), and interpret the types with Actris channels.
Why I thought this might be interesting?
- I wanted to learn Actris
- The type system fundamentally requires higher-order channels (something that is well supported in Actris)
- It shows an example of "non-manifest" sharing, where one endpoint (a "server") is shared among clients, but all the client-server interactions are totally disjoint from each other.
Overview of changes in this PR:
- Some facts about substitutions; the `is_closed_expr_set` was taken from ReLoC.
- A lemma about `big_sepM2`.
- In order to implement this "non-manifest sharing" (for the interpretation of `! A` types) I had to tweak the iProto_owns definition and formulate a log-atomic style specifications for the `send` operation.
I think the first two items are orthogonal to Actris/DILL so it might sense to see if those results can be generalized and move upstream.https://gitlab.rts.mpi-sws.org/iris/actris/-/merge_requests/27Added close definition and spec2022-04-20T11:20:37ZJonas KastbergAdded close definition and specAdded a definition and specification for "closing" channels.
The idea is that a channel endpoint, once it reaches `END` can guarantee that its _inbound_ buffer (i.e. `vsr` for `Left`, and `vsl` for `Right`) is empty, and is no longer use...Added a definition and specification for "closing" channels.
The idea is that a channel endpoint, once it reaches `END` can guarantee that its _inbound_ buffer (i.e. `vsr` for `Left`, and `vsl` for `Right`) is empty, and is no longer used by either party.
As such, it can Free the buffer (using the primitive `Free` instruction) to deallocate the memory.
In doing so, it gives up its endpoint ownership `c >-> END`.
This is achieved by changing the channel invariant to either hold the buffers, or the terminated channel endpoint:
```
Definition iProto_mapsto_def `{!heapGS Σ, !chanG Σ}
(c : val) (p : iProto Σ) : iProp Σ :=
∃ γ s (l r : loc) (lk : val),
⌜ c = ((#(side_elim s l r), #(side_elim s r l)), lk)%V ⌝ ∗
is_lock (chan_lock_name γ) lk (∃ vsl vsr,
(llist internal_eq l vsl ∨ iProto_own (chan_proto_name γ) Right END%proto) ∗
(llist internal_eq r vsr ∨ iProto_own (chan_proto_name γ) Left END%proto) ∗
steps_lb (length vsl) ∗ steps_lb (length vsr) ∗
iProto_ctx (chan_proto_name γ) vsl vsr) ∗
iProto_own (chan_proto_name γ) s p.
```
The proof relies on three observations:
- We can always receive (e.g. on `vsr` for `Left`), as we can derive a contradiction between our local endpoint ownership, and the one in the invariant. (new lemma `iProto_own_exclusive`)
- We can always send (e.g. on `vsl` for `Left`), as we can derive that whenever one protocol is sending (i.e. `(<! xs> MSG v {{ P }} ; p`), then the other protocol has _not_ terminated (i.e. it is _not_ `END`), and so it cannot be in the invariant. (new lemmas `iProto_interp_send_end_inv_{l,r}`)
- When our endpoint is `END`, the inbound buffer is always empty, and so we can close it without worrying about leftover resources (new lemmas `iProto_interp_end_inv_{l,r}`).
EDIT: Closed the outstanding lemmashttps://gitlab.rts.mpi-sws.org/iris/actris/-/merge_requests/30WIP: step_proto abstraction2023-05-22T10:21:30ZJonas KastbergWIP: step_proto abstractionThis merge request hides the multiple laters that arise from using the Actris Ghost Theory, via a "step-taking" modality `|~~> P`,
that captures the obligation to take a step _of the operational semantics_.
One motivation for this is be...This merge request hides the multiple laters that arise from using the Actris Ghost Theory, via a "step-taking" modality `|~~> P`,
that captures the obligation to take a step _of the operational semantics_.
One motivation for this is being able to present the abstraction in a way that requires less explanation.
The MR depends on the following outstanding MR of the Iris development https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/887https://gitlab.rts.mpi-sws.org/iris/actris/-/merge_requests/31Added Miniactris2023-03-20T13:54:07ZJonas KastbergAdded Miniactrishttps://gitlab.rts.mpi-sws.org/iris/actris/-/merge_requests/38Simplified recv_spec2024-03-26T17:33:59ZJonas KastbergSimplified recv_spec