Added close definition and spec (!27) · Merge requests · Iris / Actris

Open Jonas Kastberg requested to merge close_spec into master 2 years ago

All threads resolved!

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}).