Commit 1130d468 authored by Jonas Kastberg's avatar Jonas Kastberg

Merge branch 'daniel/headers' into 'master'

File headers

See merge request !16
parents ee0d1bfc 5da00edc
Pipeline #27751 passed with stage
in 5 minutes and 44 seconds
......@@ -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.
......
......@@ -2,23 +2,46 @@
separation protocols and the various operations on it like dual, append, and
branching.
Dependent separation protocols are defined by instantiating the parameterized
version in [proto_model] with type of propositions [iProp] of Iris. We define
ways of constructing instances of the instantiated type via two constructors:
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 a continuation to construct
the corresponding message protocols.
- [iProto_message], which takes an [action] and an [iMsg] which 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].
- [<!> x1 .. xn, MSG v; {{ P }}; prot] and [<?> x1 .. xn, MSG v; {{ P }}; prot],
which construct an instance of [iProto_message] with the appropriate
continuation.
- [∃ x,m] which is [iMsg_exist] with argument m.
- [MSG v ; {{ P }}; prot] which is [iMsg_Base with
- [<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 as described in proto_model.v
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
......@@ -210,25 +233,6 @@ Arguments iProto_dual_if {_ _} _ _%proto.
Instance: Params (@iProto_dual_if) 3 := {}.
(** * Protocol entailment *)
(* The definition [iProto_le] generalizes the following inductive definition
for subtyping on session types:
p1 <: p2 p1 <: p2
---------- ---------------- ----------------
end <: end !A.p1 <: !A.p2 ?A.p1 <: ?A.p2
p1 <: !B.p3 ?A.p3 <: 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
*)
Definition iProto_le_pre {Σ V}
(rec : iProto Σ V iProto Σ V iProp Σ) (p1 p2 : iProto Σ V) : iProp Σ :=
(p1 END p2 END)
......
From actris.logrel Require Export term_types.
(** This file contains definitions related to type environments. The following
relations on environments are defined:
- [env_ltyped Γ vs]: This relation indicates that the value map [vs] contains a
value for each type in the semantic type environment [Γ].
- [env_split Γ Γ1 Γ2]: The semantic type environment [Γ] can be split into
(semantically disjoint) [Γ1] and [Γ2].
- [env_copy Γ Γ']: [Γ'] is a copyable sub-environment of [Γ].
In addition, some lemmas about these definitions are proved, corresponding to
the syntactic typing rules that are typically found in linear/affine type
systems. *)
From actris.logrel Require Export term_types subtyping.
From iris.proofmode Require Import tactics.
Notation "<![ b := x ]!>" :=
......
(** This file contains a proof that the program
λ c, (recv c ||| recv c)
can be assigned the semantic type
chan (?int.?int.end) ⊸ (int * int)
This cannot be shown directly using the semantic typing rules, and therefore
manual proof is used to show that the program is semantically well-typed. This
demonstrates the extensibility of the type system. *)
From iris.algebra Require Import frac auth excl updates.
From iris.heap_lang.lib Require Export par spin_lock.
From actris.channel Require Import proofmode.
......
(** This file contains shows that the program
λ c, (recv c, recv c)
can be assigned the type
chan (?int.?int.end) ⊸ (int * int)
by exclusively using the semantic typing rules. *)
From actris.logrel Require Export term_typing_rules.
From iris.proofmode Require Import tactics.
......
(** This file defines kinded telescopes, which are used for representing binders
in session types. *)
From stdpp Require Import base tactics telescopes.
From actris.logrel Require Import model.
Set Default Proof Using "Type".
......
(** This file defines a new semantic type former [mutex A], which is the type of
mutexes containing a value of type [A]. Mutexes are copyable, regardless of
whether the type contained in them is copyable. This makes them very useful for
sharing affine resources (such as channels) between multiple threads.
Internally, mutexes are implemented using a spin lock and a mutable reference.
The operations for spin locks that are used by the mutex are defined in Iris.
The following operations are supported on mutexes:
- [mutex_alloc]: Takes a value and wraps it in a mutex.
- [mutex_acquire]: Acquire the mutex and return the value contained in it.
- [mutex_release]: Release the mutex, storing a given value in it.
The typing rules for these operations additionally contain a type
[mutexguard A], which represents a mutex that has been acquired. The typing
rules for the operations require the [mutex] or [mutexguard] to be in a variable
(i.e., let-bound), and the type of this variable in the typing context changes
as the mutex is acquired and released.
It is only possible to release a mutex after it has been opened. The
[mutexguard A] is not copyable, since that would allow a mutex to be released
multiple times after acquiring it once.
This type former is strongly inspired by the [Mutex] type in the standard
library of Rust, which has also been semantically modelled in the LambdaRust
project.
*)
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Export spin_lock.
From actris.logrel Require Export term_types term_typing_judgment subtyping.
......
(** This file contains the definition of what semantic term types and semantic
session types are. A semantic term type is a unary (Iris) predicate on values
[val → iProp], as is customary in a logical relation for type soundness.
A semantic session type is an Actris protocol [iProto].
There is a single kinded variant [lty Σ k], which contains either a term type or a
session type, depending on the kind [k]. The reason for having a single type
containing both term types and session types is that it allows for uniform
definitions of polymorphic binders for term types and session types, instead of
having duplicated definitions.
This file also defines a COFE structure on semantic term types and session
types, which is required in order to define recursive term types and session
types. *)
From iris.algebra Require Export ofe.
From actris.channel Require Export channel.
......
(** This file defines semantic typing lemmas for the operators of the language.
*)
From actris.logrel Require Export term_types.
From iris.heap_lang Require Import proofmode.
......@@ -26,7 +28,7 @@ Section operators.
Proof. iIntros (v). by iDestruct 1 as (b) "->". Qed.
Global Instance lty_int_unboxed : LTyUnboxed (Σ:=Σ) lty_int.
Proof. iIntros (v). by iDestruct 1 as (i) "->". Qed.
Global Instance lty_ref_mut_unboxed `{heapG Σ} A : LTyUnboxed (ref_mut A).
Global Instance lty_ref_uniq_unboxed `{heapG Σ} A : LTyUnboxed (ref_uniq A).
Proof. iIntros (v). by iDestruct 1 as (i w ->) "?". Qed.
Global Instance lty_ref_shr_unboxed `{heapG Σ} A : LTyUnboxed (ref_shr A).
Proof. iIntros (v). by iDestruct 1 as (l ->) "?". Qed.
......
(** This file defines the semantic interpretations of session types as Actris
protocols. It includes session types for sending and receiving with session
polymorphism, as well as n-ary choice. Recursive protocols are defined in
the model.v file. *)
From iris.algebra Require Export gmap.
From actris.logrel Require Export model kind_tele.
From actris.channel Require Export channel.
......
From actris.logrel Require Export model.
(** This file contains the definition of the semantic subtyping relation
[A <: B], where [A] and [B] can be either term types or session types, as
well as a semantic type equivalence relation [A <:> B], which is essentially
equivalent to having both [A <: B] and [B <: A]. Finally, the notion of a
*copyable type* is defined in terms of subtyping: a type [A] is copyable
when [A <: copy A]. *)
From actris.logrel Require Export model term_types.
Definition lty_le {Σ k} : lty Σ k lty Σ k iProp Σ :=
match k with
......@@ -15,6 +21,10 @@ Arguments lty_bi_le : simpl never.
Infix "<:>" := lty_bi_le (at level 70) : bi_scope.
Instance: Params (@lty_bi_le) 2 := {}.
Definition lty_copyable {Σ} (A : ltty Σ) : iProp Σ :=
tc_opaque (A <: lty_copy A)%I.
Instance: Params (@lty_copyable) 1 := {}.
Section subtyping.
Context {Σ : gFunctors}.
......@@ -31,4 +41,9 @@ Section subtyping.
Proof. solve_proper. Qed.
Global Instance lty_bi_le_proper {k} : Proper (() ==> () ==> ()) (@lty_bi_le Σ k).
Proof. solve_proper. Qed.
Global Instance lty_copyable_plain A : Plain (@lty_copyable Σ A).
Proof. rewrite /lty_copyable /=. apply _. Qed.
Global Instance lty_copyable_ne : NonExpansive (@lty_copyable Σ).
Proof. rewrite /lty_copyable /=. solve_proper. Qed.
End subtyping.
(** This file defines all of the semantic subtyping rules for term types and
session types. *)
From iris.bi.lib Require Import core.
From iris.base_logic.lib Require Import invariants.
From iris.proofmode Require Import tactics.
......@@ -213,9 +215,9 @@ Section subtyping_rules.
iApply "Hcopy".
Qed.
Lemma lty_le_ref_mut A1 A2 :
Lemma lty_le_ref_uniq A1 A2 :
(A1 <: A2) -
ref_mut A1 <: ref_mut A2.
ref_uniq A1 <: ref_uniq A2.
Proof.
iIntros "#H1" (v) "!>". iDestruct 1 as (l w ->) "[Hl HA]".
iDestruct ("H1" with "HA") as "HA".
......
(** This file contains the definitions of the semantic interpretations of the
term type formers of the type system. The semantic interpretation of a type
(former) is a unary Iris predicate on values [val → iProp], which determines
when a value belongs to a certain type.
The following types are defined:
- [unit], [bool], [int]: basic types for unit, boolean and integer values,
respectively.
- [any]: inhabited by all values.
- [A ⊸ B]: the type of affine functions from [A] to [B]. Affine functions can
only be invoked once, since they might have captured affine resources.
- [A → B]: the type of non-affine (copyable) functions from [A] to [B]. These
can be invoked any number of times. This is simply syntactic sugar for
[copy (A ⊸ B)].
- [A * B], [A + B], [∀ X, A], [∃ X, A]: products, sums, universal types,
existential types.
- [copy A]: inhabited by those values in the type [A] which are copyable. In the
case of functions, for instance, functions (closures) which capture affine
resources are not copyable, whereas functions that do not capture resources are.
- [copy- A]: acts as a kind of "inverse" to [copy A]. More precisely, we have
that [copy- (copy A) <:> A]. This type is used to indicate the results of
operations that might consume a resource, but do not always do so, depending
on whether the type [A] is copyable. Such operations result in a [copy- A],
which can be turned into an [A] using subtyping when [A] is copyable.
- [ref_uniq A]: the type of uniquely-owned mutable references to a value of type [A].
Since the reference is guaranteed to be unique, it's possible for the type [A]
contained in the reference to change to a different type [B] by assigning to
the reference.
- [ref_shr A]: the type of shared mutable references to a value of type [A].
- [chan P]: the type of channels, governed by the session type [P].
In addition, some important properties, such as contractivity and
non-expansiveness of these type formers is proved. This is important in order to
use these type formers to define recursive types. *)
From iris.bi.lib Require Import core.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Export spin_lock.
From actris.logrel Require Export subtyping kind_tele.
From actris.logrel Require Export model kind_tele.
From actris.channel Require Export channel.
Definition lty_any {Σ} : ltty Σ := Ltty (λ w, True%I).
Definition lty_copy {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, ltty_car A w)%I.
Definition lty_copy_minus {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, coreP (ltty_car A w)).
Definition lty_copyable {Σ} (A : ltty Σ) : iProp Σ :=
tc_opaque (A <: lty_copy A)%I.
Definition lty_unit {Σ} : ltty Σ := Ltty (λ w, w = #() %I).
Definition lty_bool {Σ} : ltty Σ := Ltty (λ w, b : bool, w = #b )%I.
Definition lty_int {Σ} : ltty Σ := Ltty (λ w, n : Z, w = #n )%I.
Definition lty_any {Σ} : ltty Σ := Ltty (λ w, True%I).
Definition lty_arr `{heapG Σ} (A1 A2 : ltty Σ) : ltty Σ := Ltty (λ w,
v, ltty_car A1 v - WP w v {{ ltty_car A2 }})%I.
......@@ -29,7 +57,10 @@ Definition lty_forall `{heapG Σ} {k} (C : lty Σ k → ltty Σ) : ltty Σ :=
Definition lty_exist {Σ k} (C : lty Σ k ltty Σ) : ltty Σ :=
Ltty (λ w, A, ltty_car (C A) w)%I.
Definition lty_ref_mut `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
Definition lty_copy {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, ltty_car A w)%I.
Definition lty_copy_minus {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, coreP (ltty_car A w)).
Definition lty_ref_uniq `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
(l : loc) (v : val), w = #l l v ltty_car A v)%I.
Definition ref_shrN := nroot .@ "shr_ref".
Definition lty_ref_shr `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
......@@ -40,13 +71,12 @@ Definition lty_chan `{heapG Σ, chanG Σ} (P : lsty Σ) : ltty Σ :=
Instance: Params (@lty_copy) 1 := {}.
Instance: Params (@lty_copy_minus) 1 := {}.
Instance: Params (@lty_copyable) 1 := {}.
Instance: Params (@lty_arr) 2 := {}.
Instance: Params (@lty_prod) 1 := {}.
Instance: Params (@lty_sum) 1 := {}.
Instance: Params (@lty_forall) 2 := {}.
Instance: Params (@lty_sum) 1 := {}.
Instance: Params (@lty_ref_mut) 2 := {}.
Instance: Params (@lty_ref_uniq) 2 := {}.
Instance: Params (@lty_ref_shr) 2 := {}.
Instance: Params (@lty_chan) 3 := {}.
......@@ -66,7 +96,7 @@ Notation "∀ A1 .. An , C" :=
Notation "∃ A1 .. An , C" :=
(lty_exist (λ A1, .. (lty_exist (λ An, C%lty)) ..)) : lty_scope.
Notation "'ref_mut' A" := (lty_ref_mut A) (at level 10) : lty_scope.
Notation "'ref_uniq' A" := (lty_ref_uniq A) (at level 10) : lty_scope.
Notation "'ref_shr' A" := (lty_ref_shr A) (at level 10) : lty_scope.
Notation "'chan' A" := (lty_chan A) (at level 10) : lty_scope.
......@@ -80,11 +110,6 @@ Section term_types.
Global Instance lty_copy_minus_ne : NonExpansive (@lty_copy_minus Σ).
Proof. solve_proper. Qed.
Global Instance lty_copyable_plain A : Plain (lty_copyable A).
Proof. rewrite /lty_copyable /=. apply _. Qed.
Global Instance lty_copyable_ne : NonExpansive (@lty_copyable Σ).
Proof. rewrite /lty_copyable /=. solve_proper. Qed.
Global Instance lty_arr_contractive `{heapG Σ} n :
Proper (dist_later n ==> dist_later n ==> dist n) lty_arr.
Proof.
......@@ -122,9 +147,9 @@ Section term_types.
Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist Σ k).
Proof. solve_proper. Qed.
Global Instance lty_ref_mut_contractive `{heapG Σ} : Contractive lty_ref_mut.
Global Instance lty_ref_uniq_contractive `{heapG Σ} : Contractive lty_ref_uniq.
Proof. solve_contractive. Qed.
Global Instance lty_ref_mut_ne `{heapG Σ} : NonExpansive lty_ref_mut.
Global Instance lty_ref_uniq_ne `{heapG Σ} : NonExpansive lty_ref_uniq.
Proof. solve_proper. Qed.
Global Instance lty_ref_shr_contractive `{heapG Σ} : Contractive lty_ref_shr.
......
(** This file contains the definitions of the semantic typing relation
[Γ ⊨ e : A ⫤ Γ'], indicating that in context [Γ], the expression [e] has type
[A], producing a new context [Γ']. The context is allowed to change to
accomodate things like changing the type of a channel after a receive.
In addition, we use the adequacy of Iris in order to show type soundness:
programs which satisfy the semantic typing relation are safe. That is,
semantically well-typed programs do not get stuck. *)
From iris.heap_lang Require Import metatheory adequacy.
From actris.logrel Require Export term_types.
From actris.logrel Require Import environments.
......
(** This file defines all of the semantic typing lemmas for term types. Most of
these lemmas are semantic versions of the syntactic typing judgments typically
found in a syntactic type system. *)
From stdpp Require Import pretty.
From iris.bi.lib Require Import core.
From iris.base_logic.lib Require Import invariants.
......@@ -255,11 +258,10 @@ Section properties.
iIntros (w) "[$ HΓ3]". by iApply env_ltyped_delete.
Qed.
(** Mutable Reference properties *)
(** Mutable Unique Reference properties *)
Lemma ltyped_alloc Γ1 Γ2 e A :
(Γ1 e : A Γ2) -
(Γ1 ref e : ref_mut A Γ2).
(Γ1 ref e : ref_uniq A Γ2).
Proof.
iIntros "#He" (vs) "!> HΓ1 /=".
wp_bind (subst_map vs e).
......@@ -270,8 +272,8 @@ Section properties.
Qed.
Lemma ltyped_load Γ (x : string) A :
Γ !! x = Some (ref_mut A)%lty
Γ ! x : A <[x := (ref_mut (copy- A))%lty]> Γ.
Γ !! x = Some (ref_uniq A)%lty
Γ ! x : A <[x := (ref_uniq (copy- A))%lty]> Γ.
Proof.
iIntros (Hx vs) "!> HΓ".
iDestruct (env_ltyped_lookup with "HΓ") as (v Hv) "[HA HΓ]"; first done.
......@@ -281,7 +283,7 @@ Section properties.
iAssert (ltty_car (copy- A) w)%lty as "#HAm".
{ iApply coreP_intro. iApply "Hw". }
iFrame "Hw".
iAssert (ltty_car (ref_mut (copy- A))%lty #l) with "[Hl]" as "HA".
iAssert (ltty_car (ref_uniq (copy- A))%lty #l) with "[Hl]" as "HA".
{ iExists l, w. iSplit=>//. iFrame "Hl HAm". }
iDestruct (env_ltyped_insert _ _ x with "HA HΓ") as "HΓ".
rewrite /binder_insert insert_delete (insert_id _ _ _ Hv).
......@@ -289,9 +291,9 @@ Section properties.
Qed.
Lemma ltyped_store Γ Γ' (x : string) e A B :
Γ' !! x = Some (ref_mut A)%lty
Γ' !! x = Some (ref_uniq A)%lty
(Γ e : B Γ') -
Γ x <- e : () <[x := (ref_mut B)%lty]> Γ'.
Γ x <- e : () <[x := (ref_uniq B)%lty]> Γ'.
Proof.
iIntros (Hx) "#He". iIntros (vs) "!> HΓ /=".
wp_bind (subst_map vs e).
......@@ -300,16 +302,16 @@ Section properties.
rewrite Hw.
iDestruct "HA" as (l v' ->) "[Hl HA]".
wp_store. iSplitR; first done.
iAssert (ltty_car (ref_mut B)%lty #l) with "[Hl HB]" as "HB".
iAssert (ltty_car (ref_uniq B)%lty #l) with "[Hl HB]" as "HB".
{ iExists l, v. iSplit=>//. iFrame "Hl HB". }
iDestruct (env_ltyped_insert _ _ x with "HB HΓ'") as "HΓ'".
rewrite /binder_insert insert_delete (insert_id _ _ _ Hw).
iFrame "HΓ'".
Qed.
(** Shared Reference properties *)
(** Mutable Shared Reference properties *)
Lemma ltyped_upgrade_shared Γ Γ' e A :
(Γ e : ref_mut (copy A) Γ') -
(Γ e : ref_uniq (copy A) Γ') -
Γ e : ref_shr A Γ'.
Proof.
iIntros "#He" (vs) "!> HΓ". iApply wp_fupd.
......@@ -397,6 +399,7 @@ Section properties.
Qed.
End with_spawn.
(** Channel properties *)
Section with_chan.
Context `{chanG Σ}.
......
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