Commit 9456e121 authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

Updated header for channel.v

parent 0c8b2e21
......@@ -17,7 +17,10 @@ In this file we define the three message-passing connectives:
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.*)
which it pops and returns, locking during each peek.
It is additionaly shown that the channel ownership [c ↣ prot] is closed under
the subprotocol relation [⊑] *)
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang Require Import proofmode.
From iris.heap_lang.lib Require Import spin_lock.
......@@ -27,7 +27,7 @@ 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 as described in proto_model.v
In addition we define the [iProto_le] subprotocol relation, which generalises
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
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