diff --git a/.gitignore b/.gitignore index 6206b44..e05ea00 100644 --- a/.gitignore +++ b/.gitignore @@ -18,3 +18,4 @@ MAlonzo/ # Ignore our generated main file src/Examples/Main-generated.agda +src/Selective/Examples/Main-generated.agda diff --git a/Makefile b/Makefile index 3e1eefe..be07352 100644 --- a/Makefile +++ b/Makefile @@ -23,6 +23,12 @@ selective-generated-main: sed 's/__ENTRY__/$(ENTRY)/' src/Selective/Examples/Main-template.agda > src/Selective/Examples/Main-generated.agda stack exec agda -- -c src/Selective/Examples/Main-generated.agda +test-that-all-compliles: + $(MAKE) latex-clean + $(MAKE) latex + stack exec agda -- --no-main -c src/Selective/Examples/Main-generated.agda + stack exec agda -- --no-main -c src/Examples/Main-generated.agda + clean: ifneq ($(strip $(agda-objects)),) rm $(agda-objects) diff --git a/latex.make b/latex.make index e95b6fe..c2fd338 100644 --- a/latex.make +++ b/latex.make @@ -9,8 +9,6 @@ generated := $(wildcard $(out-subdirs:%=%*.tex)) $(moved): $(LATEX-OUTPUT-DIR)%.tex: src/%.lagda.tex stack exec agda -- --latex-dir=$(LATEX-OUTPUT-DIR) --latex $< - perl postprocess-latex.pl $@ > $(LATEX-OUTPUT-DIR)$*.processed - mv $(LATEX-OUTPUT-DIR)$*.processed $@ .PHONY: all clean all: $(moved) diff --git a/src/ActorMonad.lagda.tex b/src/ActorMonad.lagda.tex index a3c53f6..26a3cad 100644 --- a/src/ActorMonad.lagda.tex +++ b/src/ActorMonad.lagda.tex @@ -26,10 +26,6 @@ we can make sure that every message read from the inbox has a valid type. In terms of \textcite{DBLP:conf/agere/KosterCM16}, this is the interface of the actor. -\AgdaTarget{MessageType} -\AgdaTarget{ValueType} -\AgdaTarget{ReferenceType} -\AgdaTarget{InboxShape} \begin{code} mutual data MessageField : Set₁ where @@ -42,27 +38,27 @@ \end{code} We define the type of an actor's inbox as an algebraic data-type with sums -(\AgdaRef[ActorMonad]{InboxShape}) of products (\AgdaRef[ActorMonad]{MessageType}). -The \AgdaRef[ActorMonad]{InboxShape} is a variant type that details +(\AgdaFunction{InboxShape}) of products (\AgdaFunction{MessageType}). +The \AgdaFunction{InboxShape} is a variant type that details all the messages that can be received from an inbox. Every message sent to an actor will have exactly one of the types that is listed, which we communicate as a tag attached to the message (see section \ref{sec:messages}). -We can think of the \AgdaRef[ActorMonad]{InboxShape} as a set of types, +We can think of the \AgdaFunction{InboxShape} as a set of types, and every message coming paired with a proof that the message is a type from that set. To know what type a message has you have to inspect the proof, and the fields of the message will become accessible. -\AgdaRef[ActorMonad]{MessageType} also uses a list as its underlying data structure, +\AgdaFunction{MessageType} also uses a list as its underlying data structure, but for a rather different purpose. -\AgdaRef[ActorMonad]{MessageType} is the type of a single message, +\AgdaFunction{MessageType} is the type of a single message, and every element in the list represents a single field in a record. -\AgdaRef[ActorMonad]{MessageType} should thus be seen as a product type, +\AgdaFunction{MessageType} should thus be seen as a product type, similar to Haskell's tuples. -The fields in \AgdaRef[ActorMonad]{MessageType} are combinations of value types and reference types. +The fields in \AgdaFunction{MessageType} are combinations of value types and reference types. A value type is any type from Agda's lowest set universe. -Typical examples are \AgdaRef[Examples/Types]{Bool}, \AgdaRef[Examples/Types]{ℕ}, -or \AgdaRef[Examples/Types]{⊤}. +Typical examples are \AgdaDatatype{Bool}, \AgdaDatatype{ℕ}, +or \AgdaRecord{⊤}. We limit the types to the lowest set universe as a sort of approximation of serializable values. It would be possible to further constrain the types to only those that are serializable, but due to its insignificance to the calculus we have opted not to. @@ -78,7 +74,7 @@ Typically, the reference type of a field should be the smallest set of types that will be sent using that reference. -Below we have created an instance of an \AgdaRef[ActorMonad]{InboxShape}, +Below we have created an instance of an \AgdaFunction{InboxShape}, showcasing the important concepts. \AgdaFunction{TestInbox} is an inbox that can receive two kinds of messages: messages containing a single boolean value, @@ -107,14 +103,14 @@ to break the type of inboxes into granular subtypes. Subtyping of inboxes means that given two inboxes $A$ and $B$, if $A <: B$, then every message in $A$ is also a valid message in $B$. -Since we model \AgdaRef[ActorMonad]{InboxShape} as a set, +Since we model \AgdaFunction{InboxShape} as a set, the subtype relation can be taken to just be the subset relation. \begin{code} _<:_ = _⊆_ {A = MessageType} \end{code} -Our representation of subsets uses two datastructures: \AgdaDatatype{∈} and \AgdaDatatype{⊆}. +Our representation of subsets uses two data structures: \AgdaDatatype{∈} and \AgdaDatatype{⊆}. \AgdaDatatype{∈} is the list or set membership relation, which we model as a Peano number that tells at what position the element occurs in the list. An element that appears at the head of a list is at index \AgdaInductiveConstructor{Z}, @@ -131,7 +127,7 @@ of the lists in question. A view is a datatype that reveals something interesting about its indices, \eg that a list is a subset of another. To define \AgdaDatatype{⊆} we state that the empty list (\AgdaInductiveConstructor{[]}) is a subset of all lists, -and we state that to you can add an element to a subset (\AgdaInductiveConstructor{∷}) if you +and we state that you can add an element to a subset (\AgdaInductiveConstructor{∷}) if you are able to prove that the element is a member of the other set. \AgdaCatch{Membership}{Subset} @@ -146,7 +142,7 @@ %<*ActorPrecondition> It is crucial that actor references are completely unforgeable if type safety is to be preserved. -If an actor is allowed to manufacture references on their own, +If an actor is allowed to manufacture references on its own, every guarantee we have about message types becomes invalid and unusable. Allowing either the name or the type of a reference to be controlled in user space makes it possible to create a reference to an inbox that is incompatible with the underlying inbox, @@ -187,15 +183,15 @@ Renaming the variables of an expression in a way that preserves α-equivalence is called α-renaming \parencite{turbak2008design}. α-renaming is a part of the general concept of substitution, -the operation of replacing free occurances of a varibale with an expression. -The role of α-renaming in substituion is to avoid accidental variable name captures by renaming +the operation of replacing free occurrences of a variable with an expression. +The role of α-renaming in substitution is to avoid accidental variable name captures by renaming variables so that substitution does not change the meaning of functions \parencite{turbak2008design}. In order to avoid the problem of α-equivalence and α-renaming, a common formalization technique is the use of de Bruijn indices to represent variable binders \parencite{DBLP:journals/entcs/BerghoferU07}. -A de Bruijn index is a natural number that represents an occurance of a variable in a λ-term, -and denotes the number of binders that are in scope between that occurance +A de Bruijn index is a natural number that represents an occurrence of a variable in a λ-term, +and denotes the number of binders that are in scope between that occurrence and its corresponding binder. Following are some examples comparing a λ-calculus with names and a λ-calculus using de Bruijn indices. @@ -215,10 +211,9 @@ (de Bruijn) indices into that list. We choose to represent the indices as the membership proposition in order to make the de Bruijn indices correct by construction. -This let's us define the type judgement $Γ ⊢ T$ as: +This lets us define the type judgement $Γ ⊢ T$ as: \AgdaCatch{Membership}{ElementIn} -\AgdaTarget{ReferenceTypes} \begin{code} ReferenceTypes = List InboxShape TypingContext = ReferenceTypes @@ -251,14 +246,14 @@ The notion of a subtype for references is important to implement the pattern of sending a command together with what reference to reply to, -since different actors receiving the reply will have a different \AgdaRef[ActorMonad]{InboxShape}. +since different actors receiving the reply will have a different \AgdaFunction{InboxShape}. This pattern, together with a selective receive construct, can be used to implement synchronous calls \parencite{ericsson_gen}. % %<*Messages> Messages in \ourlang are made up of a tag, indicating the type of the message, -and instatiations of the fields in that message type. +and instantiations of the fields in that message type. We have made the unusual decision to give outgoing and incoming messages slightly different shapes. This choice is purely for ease of implementation and does not affect the power of the model. @@ -267,9 +262,9 @@ We index the type of a message by the type of inbox it is being sent to and incidentally by the variable typing context. Selecting which type variant this message has is done by indexing -into the \AgdaRef[ActorMonad]{InboxShape}, using the $∈$ property. +into the \AgdaFunction{InboxShape}, using the $∈$ property. The rest of the message is made up of instantiations of the fields -from the selected \AgdaRef[ActorMonad]{MessageType}. +from the selected \AgdaFunction{MessageType}. For values, the instantiation of a field is simply an Agda term of the type specified by the field. For references, the instantiation is not a simple Agda term, but rather a variable in the reference context. @@ -282,11 +277,12 @@ send-field-content Γ (ValueType A) = Lift A send-field-content Γ (ReferenceType requested) = Γ ⊢>: requested -data SendMessage (To : InboxShape) (Γ : TypingContext) : Set₁ where - SendM : {MT : MessageType} → - MT ∈ To → - All (send-field-content Γ) MT → - SendMessage To Γ +record SendMessage (To : InboxShape) (Γ : TypingContext) : Set₁ where + constructor SendM + field + {MT} : MessageType + selected-message-type : MT ∈ To + send-fields : All (send-field-content Γ) MT \end{code} Incoming messages differ from outgoing messages in the instantiation of reference fields. @@ -298,7 +294,7 @@ We will see in section \ref{sec:actorm} that the shape of the variable typing context is maintained in the type of the monad, making it easy to create indices into the variable context without making them a part of the message. -It would be possible to make the reference field content be an indicex into the variable context, +It would be possible to make the reference field content be an indices into the variable context, but it would make the model slightly more complicated without making it more powerful. @@ -308,11 +304,12 @@ receive-field-content (ValueType A) = A receive-field-content (ReferenceType Fw) = ⊤ -data Message (To : InboxShape) : Set₁ where - Msg : {MT : MessageType} → - MT ∈ To → - All receive-field-content MT → - Message To +record Message (To : InboxShape) : Set₁ where + constructor Msg + field + {MT} : MessageType + received-message-type : MT ∈ To + received-fields : All receive-field-content MT extract-references : MessageType → ReferenceTypes extract-references [] = [] @@ -327,7 +324,6 @@ infixl 1 _∞>>=_ _>>=_ _∞>>_ _>>_ \end{code} %<*LiftTop> -\AgdaTarget{⊤₁} \begin{code} ⊤₁ : Set₁ ⊤₁ = Lift ⊤ @@ -344,13 +340,13 @@ Furthermore, \textcite{DBLP:conf/ecoop/FowlerLW17} show that if the host language is sufficiently advanced selective receive can be implemented as a library, in contrast to having it as a built in primitive. -This lead to us to implement \ourlang as an embedded DSL in the form of a monad. +This led us to implement \ourlang as an embedded DSL in the form of a monad. The goal when translating $λ_{act}$ to an Agda embedding was to make the actors correct by construction, and to make it possible to type-check each actor separately. The pattern we found suitable is a monad parameterized by the type of the actor's -inbox (\AgdaRef[ActorMonad]{InboxShape}) and indexed by a reference variable context. -Following \textcite{DBLP:conf/ecoop/FowlerLW17}, the \AgdaRef[ActorMonad]{InboxShape} of an actor is +inbox (\AgdaFunction{InboxShape}) and indexed by a reference variable context. +Following \textcite{DBLP:conf/ecoop/FowlerLW17}, the \AgdaFunction{InboxShape} of an actor is constant over its lifetime and should be likened with the type-and-effect system of $λ_{act}$. Each actor has their own reference variable context and the way it changes over time is kept track of in the style of the parameterized monad pattern, @@ -360,21 +356,19 @@ Following the lead of \textcite{DBLP:journals/corr/AbelC14}, we represent the monad \AgdaDatatype{ActorM} as a mutual definition of an inductive datatype and a coinductive record. -The record \AgdaRef[ActorMonad]{∞ActorM} is a coalgebra that one interacts with by using its -single observation (copattern) \AgdaRef[ActorMonad]{force}. -\AgdaRef[ActorMonad]{force} gives us an element of the \AgdaDatatype{ActorM} datatype +The record \AgdaRecord{∞ActorM} is a coalgebra that one interacts with by using its +single observation (copattern) \AgdaField{force}. +\AgdaField{force} gives us an element of the \AgdaDatatype{ActorM} datatype on which we can pattern match to see which computation to perform next. -Both \AgdaDatatype{ActorM} and \AgdaRef[ActorMonad]{∞ActorM} are indexed by a size $i$. -The size is a lower bound on on the number of times we can iteratively \AgdaRef[ActorMonad]{force} +Both \AgdaDatatype{ActorM} and \AgdaRecord{∞ActorM} are indexed by a size $i$. +The size is a lower bound on the number of times we can iteratively \AgdaField{force} the computation, but should primarily be seen as a means to establish productivity of recursive definitions. When we actually simulate running actors, -we only care for \AgdaDatatype{ActorM} \AgdaPostulate{∞} \AgdaDatatype{A} of infinite depth. +we only care for \AgdaDatatype{ActorM}\AgdaSpace{}\AgdaPostulate{∞}\AgdaSpace{}\AgdaDatatype{A} + of infinite depth. -\AgdaTarget{ActorM} -\AgdaTarget{∞ActorM} -\AgdaTarget{force} \begin{code} data ActorM (i : Size) (IS : InboxShape) : (A : Set₁) → (pre : TypingContext) → @@ -393,20 +387,21 @@ \end{code} % %<*ActorMonadBindReturn> -Return and bind of the actor monad uses the invariants that are expected from any parameterized +Return and bind of the actor monad use the invariants that are expected from any parameterized monad, which is explained in section \ref{parameterized_monads}. Bind chains together potentially infinite sub-computations, and we can see that bind preserves the size (observation depth) $i$. Agda implements a sort of subtyping for sizes, so computations of different sizes can still be composed via bind. -We don't give the constructors \AgdaRef[ActorMonad]{Return} and \AgdaInductiveConstructor{∞>>=} -the names return and >>=, -since we want those names to refer to the type \AgdaRef[ActorMonad]{∞ActorM}. -Instead, the actual return and >>= are defined as a separate functions -that wrap \AgdaRef[ActorMonad]{Return} and \AgdaInductiveConstructor{∞>>=}. +We don't give the constructors \AgdaInductiveConstructor{Return} +and \AgdaInductiveConstructor{∞>>=} +the names return and $\Bind$, +since we want those names to refer to the type \AgdaRecord{∞ActorM}. +Instead, the actual return and $\Bind$ are defined as a separate functions +that wrap \AgdaInductiveConstructor{Return} and +\AgdaInductiveConstructor{∞>>=}. -\AgdaTarget{Return} \begin{code} Return : ∀ {A post} → (val : A) → ActorM i IS A (post val) post _∞>>=_ : ∀ {A B pre mid post} → (m : ∞ActorM i IS A pre mid) → @@ -415,10 +410,9 @@ \end{code} % %<*ActorMonadSpawn> -\AgdaRef[ActorMonad]{Spawn} creates a new actor and adds a reference to the spawned actor -to the spawning actor's variable context. +\AgdaInductiveConstructor{Spawn} creates a new actor and +adds a reference to the spawned actor to the spawning actor's variable context. The spawned actor starts with both an empty inbox and an empty variable context. -\AgdaTarget{Spawn} \begin{code} Spawn : {NewIS : InboxShape} → {A : Set₁} → ∀ {pre postN} → ActorM i NewIS A [] postN → @@ -430,11 +424,11 @@ It is not explicit in the monad what happens to a sent message, but we see in (SECTION) that evaluating Send will append the message to the actor being referenced. The reference variable might be a subtype to the underlying actor it references, -but this fact is completely opaque to the \AgdaRef[ActorMonad]{Send} construct. +but this fact is completely opaque to the +\AgdaInductiveConstructor{Send} construct. The contents of the message is detailed in section \ref{sec:messages}. Sending a message does of course not affect the variable context, which is captured in the postcondition being the same as the precondition. -\AgdaTarget{Send} \begin{code} Send : ∀ {pre} → {ToIS : InboxShape} → (canSendTo : pre ⊢ ToIS) → @@ -443,16 +437,15 @@ \end{code} % %<*ActorMonadReceive> -The \AgdaRef[ActorMonad]{Receive} construct is an operation that optimistically tries to -retrieve a message from the actor's inbox. +The \AgdaInductiveConstructor{Receive} construct is an operation +that optimistically tries to retrieve a message from the actor's inbox. Messages are retrieved in the order they are added to the inbox, and in the case of an empty inbox the actor is paused indefinitely. As discussed in section \ref{sec:messages}, every reference in the received message will be added to the actor's variable context. -\AgdaRef[ActorMonad]{Receive} is the only construct that have a postcondition that depends on +\AgdaInductiveConstructor{Receive} is the only construct that has a postcondition that depends on run-time behaviour, so a model where references are handled differently could allow for actors to be implemented as non-parameterized monads. -\AgdaTarget{Receive} \begin{code} Receive : ∀ {pre} → ActorM i IS (Message IS) pre (add-references pre) \end{code} @@ -460,10 +453,10 @@ %<*ActorMonadSelf> A key concept in Erlang-style actors is that actors can easily get a reference to themselves. For example, in order to implement callbacks the initiating actor must include a reference -to themselves for the corresponding actor to reply to. -In \AgdaDatatype{ActorM}, this need is fulfilled by the \AgdaRef[ActorMonad]{Self} construct, +to itself for the corresponding actor to reply to. +In \AgdaDatatype{ActorM}, this need is fulfilled by the +\AgdaInductiveConstructor{Self} construct, which adds a reference to the actor itself to the variable context. -\AgdaTarget{Self} \begin{code} Self : ∀ {pre} → ActorM i IS ⊤₁ pre (λ _ → IS ∷ pre) \end{code} @@ -478,12 +471,11 @@ make subsequent invariants compatible. What we chose to implement is similar to the strengthening rule in Hoare logic, which affects the precondition of a statement. -The operation that \AgdaRef[ActorMonad]{Strengthen} performs is a re-ordering of the variables -in the variable context. +The operation that \AgdaInductiveConstructor{Strengthen} +performs is a re-ordering of the variables in the variable context. It does so by relating the precondition to the postcondition via a subset relation. The subset relation supports re-ordering, duplication, and to forget variables, making it powerful without sacrificing correctness. -\AgdaTarget{Strengthen} \begin{code} Strengthen : ∀ {ys xs} → (inc : ys ⊆ xs) → ActorM i IS ⊤₁ xs (λ _ → ys) diff --git a/src/Colist.agda b/src/Colist.agda index c40e64b..3e719f9 100644 --- a/src/Colist.agda +++ b/src/Colist.agda @@ -7,7 +7,7 @@ data Colist (i : Size) {a} (A : Set a) : Set a record ∞Colist (i : Size) {a} (A : Set a) : Set a where coinductive constructor delay_ - field force : ∀ {j : Size< i} → Colist i A + field force : ∀ {j : Size< i} → Colist j A data Colist (i : Size) {a} (A : Set a) where [] : Colist i A diff --git a/src/Cont.agda b/src/Cont.agda deleted file mode 100644 index 6740d7f..0000000 --- a/src/Cont.agda +++ /dev/null @@ -1,48 +0,0 @@ - -module Cont where - -open import ActorMonad -open import SimulationEnvironment -open import Membership using (_∈_ ; _⊆_ ; [] ; _∷_ ; Z ; S ; lookup-parallel ; lookup-parallel-≡ ; translate-∈ ; x∈[]-⊥ ; translate-⊆ ; ⊆-trans ; find-∈) - -open import Data.List using (List ; _∷_ ; [] ; map ; _++_ ; drop) -open import Data.List.All using (All ; _∷_ ; []; lookup) renaming (map to ∀map) -open import Data.List.All.Properties using (++⁺ ; drop⁺) -open import Data.List.Properties using (map-++-commute) -open import Data.List.Any using (Any ; here ; there) -open import Data.Nat using (ℕ ; zero ; suc ; _≟_ ; _<_) -open import Data.Nat.Properties using (≤-reflexive) -open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) -open import Data.Unit using (⊤ ; tt) -open import Data.Empty using (⊥ ; ⊥-elim) - -open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; cong ; cong₂ ; trans) -open import Relation.Nullary using (Dec ; yes ; no) - -open import Level using (Lift ; lift) -open import Size using (Size; ∞) - -open Actor -open ValidActor -open Env -open NamedInbox - - -Cont : ∀ (i : Size) (IS : InboxShape) {A B : Set₁} - (pre : A → TypingContext) - (post : B → TypingContext) → - Set₂ -Cont i IS {A} {B} pre post = (x : A) → ∞ActorM i IS B (pre x) post - -data ContStack (i : Size) (IS : InboxShape) {A : Set₁} (pre : A → TypingContext) : - ∀ {B : Set₁} (post : B → TypingContext) → Set₂ where - [] : ContStack i IS pre pre - _∷_ : ∀{B C}{mid : B → TypingContext} {post : C → TypingContext} - → Cont i IS pre mid → ContStack i IS mid post → ContStack i IS pre post - -record ActorState (i : Size) (IS : InboxShape) (C : Set₁) (pre : TypingContext) (post : C → TypingContext) : Set₂ where - field - {A} : Set₁ - {mid} : A → TypingContext - act : ActorM i IS A pre mid - cont : ContStack i IS mid post diff --git a/src/EnvironmentOperations.agda b/src/EnvironmentOperations.agda index b5b746c..68698f0 100644 --- a/src/EnvironmentOperations.agda +++ b/src/EnvironmentOperations.agda @@ -1,7 +1,7 @@ module EnvironmentOperations where open import ActorMonad open import SimulationEnvironment -open import Membership using (_∈_ ; _⊆_ ; [] ; _∷_ ; Z ; S ; lookup-parallel ; lookup-parallel-≡ ; translate-∈ ; x∈[]-⊥ ; translate-⊆ ; ⊆-trans ; find-∈) +open import Membership using (_∈_ ; _⊆_ ; [] ; _∷_ ; Z ; S ; lookup-parallel ; lookup-parallel-≡ ; translate-∈ ; x∈[]-⊥ ; translate-⊆ ; ⊆-trans ; find-∈ ; All-⊆) open import Data.List using (List ; _∷_ ; [] ; map ; _++_ ; drop) open import Data.List.All using (All ; _∷_ ; []; lookup) renaming (map to ∀map) @@ -15,7 +15,7 @@ open import Data.Unit using (⊤ ; tt) open import Data.Empty using (⊥ ; ⊥-elim) open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; cong ; cong₂ ; trans) -open import Relation.Nullary using (Dec ; yes ; no) +open import Relation.Nullary using (Dec ; yes ; no ; ¬_) open import Level using (Lift ; lift) open import Size using (∞) @@ -49,13 +49,13 @@ lift-actor : (actor : Actor) → {pre : TypingContext} → Actor lift-actor actor {pre} references pre-eq-refs m = record { inbox-shape = inbox-shape actor - ; A = A actor + ; A = actor .A ; references = references ; pre = pre ; pre-eq-refs = pre-eq-refs - ; post = post actor + ; post = actor .post ; computation = m - ; name = name actor + ; name = actor .name } -- Replace the monadic part of an actor @@ -114,31 +114,97 @@ add-references-rewrite actor nms {x} p m = record ; name = name actor } +data SameValidityProof : Actor → Actor → Set₁ where + AreSame : + ∀ {A A' pre pre' post post'} + {IS name references} + {per per'} + {computation computation'} → + SameValidityProof + (record + { inbox-shape = IS + ; A = A + ; references = references + ; pre = pre + ; pre-eq-refs = per + ; post = post + ; computation = computation + ; name = name + }) + (record + { inbox-shape = IS + ; A = A' + ; references = references + ; pre = pre' + ; pre-eq-refs = per' + ; post = post' + ; computation = computation' + ; name = name + }) + -- A proof of an actor being valid is also valid for another actor if -- * they have the same name -- * they have the same references -- * they have the same inbox type rewrap-valid-actor : {store : Store} → {actorPre : Actor} → {actorPost : Actor} → + SameValidityProof actorPre actorPost → ValidActor store actorPre → - (name actorPre) ≡ (name actorPost) → - (references actorPre) ≡ (references actorPost) → - (inbox-shape actorPre) ≡ (inbox-shape actorPost) → ValidActor store actorPost -rewrap-valid-actor va refl refl refl = record { actor-has-inbox = actor-has-inbox va - ; references-have-pointer = references-have-pointer va } +rewrap-valid-actor AreSame va = record { actor-has-inbox = va .actor-has-inbox ; references-have-pointer = va .references-have-pointer } + +data ReferenceAdded (ref : NamedInbox) : Actor → Actor → Set₁ where + RefAdded : + ∀ {A A' pre pre' post post'} + {IS name references} + {per per'} + {computation computation'} → + ReferenceAdded ref + (record + { inbox-shape = IS + ; A = A + ; references = references + ; pre = pre + ; pre-eq-refs = per + ; post = post + ; computation = computation + ; name = name + }) + (record + { inbox-shape = IS + ; A = A' + ; references = ref ∷ references + ; pre = pre' + ; pre-eq-refs = per' + ; post = post' + ; computation = computation' + ; name = name + }) + +add-reference-valid : {store : Store} → {actorPre : Actor} → {actorPost : Actor} → + {ref : NamedInbox} → + ReferenceAdded ref actorPre actorPost → + ValidActor store actorPre → + reference-has-pointer store ref → + ValidActor store actorPost +add-reference-valid RefAdded va p = record { actor-has-inbox = va .actor-has-inbox ; references-have-pointer = p ∷ (va .references-have-pointer) } record ValidMessageList (store : Store) (S : InboxShape) : Set₁ where field inbox : Inbox S valid : All (message-valid store) inbox -record UpdatedInboxes (store : Store) {store' : Store} (original : Inboxes store') : Set₂ where +InboxUpdater : (store : Store) (IS : InboxShape) → Set₁ +InboxUpdater store IS = ValidMessageList store IS → ValidMessageList store IS + +record UpdatedInbox (store : Store) {store' : Store} (original : Inboxes store') (name : Name) : Set₂ where field updated-inboxes : Inboxes store' inboxes-valid : InboxesValid store updated-inboxes + others-unaffected : ∀ {name' IS' inb} → ¬ name ≡ name' → {p' : name' ↦ IS' ∈e store'} → InboxForPointer inb store' original p' → InboxForPointer inb store' updated-inboxes p' + open ValidMessageList -open UpdatedInboxes +open UpdatedInbox open NameSupply -- Update one of the inboxes in a list of inboxes. @@ -149,18 +215,29 @@ open NameSupply -- and a proof that all the messages are valid for the store. -- The update function returns a new list of the same type, -- and has to provide a proof that this list is also valid for the store -update-inboxes : {name : Name} → {IS : InboxShape} → +update-inbox : {name : Name} → {IS : InboxShape} → (store : Store) → - {store' : Store} → (inboxes : Inboxes store') → + {store' : Store} → + (inboxes : Inboxes store') → (InboxesValid store inboxes) → (name ↦ IS ∈e store') → - (f : ValidMessageList store IS → ValidMessageList store IS) → - UpdatedInboxes store inboxes -update-inboxes _ _ [] () _ -update-inboxes store (x ∷ inboxes) (px ∷ proofs) zero f with (f (record { inbox = x ; valid = px })) -... | updated = record { updated-inboxes = (inbox updated) ∷ inboxes ; inboxes-valid = (valid updated) ∷ proofs } -update-inboxes store (x ∷ inboxes) (px ∷ proofs) (suc p) f with (update-inboxes store inboxes proofs p f) -... | updated = record { updated-inboxes = x ∷ updated-inboxes updated ; inboxes-valid = px ∷ (inboxes-valid updated) } + (f : InboxUpdater store IS) → + UpdatedInbox store inboxes name +update-inbox _ _ [] () _ +update-inbox {name} store {store'} (x ∷ inboxes) (px ∷ proofs) zero f = + record { updated-inboxes = inbox updated ∷ inboxes ; inboxes-valid = (valid updated) ∷ proofs ; others-unaffected = unaffected } + where + updated = (f (record { inbox = x ; valid = px })) + unaffected : ∀ {name' IS' inb} → ¬ name ≡ name' → {p' : name' ↦ IS' ∈e store'} → InboxForPointer inb store' (x ∷ inboxes) p' → InboxForPointer inb store' (inbox updated ∷ inboxes) p' + unaffected pr zero = ⊥-elim (pr refl) + unaffected pr (suc ifp) = suc ifp +update-inbox {name} store {store'} (x ∷ inboxes) (px ∷ proofs) (suc p) f = + record { updated-inboxes = x ∷ updated-inboxes updated ; inboxes-valid = px ∷ inboxes-valid updated ; others-unaffected = unaffected } + where + updated = (update-inbox store inboxes proofs p f) + unaffected : ∀ {name' IS' inb} → ¬ name ≡ name' → {p' : name' ↦ IS' ∈e store'} → InboxForPointer inb store' (x ∷ inboxes) p' → InboxForPointer inb store' (x ∷ updated-inboxes updated) p' + unaffected pr zero = zero + unaffected pr (suc ifp) = suc (others-unaffected updated pr ifp) -- Move the actor that is at the top of the list, to the back of the list -- This is done to create a round-robin system for the actors, since run-env always picks the actor at the top @@ -178,34 +255,26 @@ top-actor-to-back env | x ∷ acts | (y ∷ prfs) = record ; blocked-valid = blocked-valid env ; messages-valid = messages-valid env ; name-supply = name-supply env + ; blocked-no-progress = blocked-no-progress env } --- Drop the actor that is at the top of the list completely. --- This is used when handling some monadic operations, when there is no following bind. --- The dropped actor is not put in the blocked list. -drop-top-actor : Env → Env -drop-top-actor env with (acts env) | (actors-valid env) -drop-top-actor env | [] | prfs = env -drop-top-actor env | _ ∷ rest | _ ∷ prfs = record - { acts = rest - ; blocked = blocked env - ; env-inboxes = env-inboxes env - ; store = store env - ; actors-valid = prfs - ; blocked-valid = blocked-valid env - ; messages-valid = messages-valid env - ; name-supply = name-supply env - } - -- An actor is still valid if we add a new inbox to the store, as long as that name is not used in the store before valid-actor-suc : ∀ {store actor IS} → (ns : NameSupply store) → ValidActor store actor → ValidActor (inbox# ns .name [ IS ] ∷ store) actor -valid-actor-suc ns va = record { - actor-has-inbox = suc {pr = ns .name-is-fresh (actor-has-inbox va)} (actor-has-inbox va) - ; references-have-pointer = ∀map (λ p → suc-p (ns .name-is-fresh (actual-has-pointer p)) p) (references-have-pointer va) - } - where - open ValidActor - open _comp↦_∈_ +valid-actor-suc ns va = + let open ValidActor + open _comp↦_∈_ + in record { + actor-has-inbox = suc {pr = ns .name-is-fresh (actor-has-inbox va)} (actor-has-inbox va) + ; references-have-pointer = ∀map (λ p → suc-p (ns .name-is-fresh (actual-has-pointer p)) p) (references-have-pointer va) + } + +valid-references-suc : ∀ {store references IS} → + (ns : NameSupply store) → + All (reference-has-pointer store) references → + All (reference-has-pointer (inbox# (ns .name) [ IS ] ∷ store)) references +valid-references-suc ns pointers = + let open _comp↦_∈_ + in ∀map (λ p → suc-p (ns .name-is-fresh (actual-has-pointer p)) p) pointers -- All the messages in an inbox are still valid if we add a new inbox to the store, as long as that name is not used in the store before messages-valid-suc : ∀ {store IS x} {inb : Inbox IS} → (ns : NameSupply store) → all-messages-valid store inb → all-messages-valid (inbox# ns .name [ x ] ∷ store) inb @@ -222,6 +291,10 @@ messages-valid-suc {store} {IS} {x} {nx ∷ _} ns (px ∷ vi) = message-valid-su message-valid-suc : (nx : NamedMessage IS) → message-valid store nx → message-valid (inbox# ns .name [ x ] ∷ store) nx message-valid-suc (NamedM x₁ x₂) px = fields-valid-suc px +is-blocked-suc : ∀ {store actor IS} {inbs : Inboxes store} {inb : Inbox IS} → (ns : NameSupply store) → IsBlocked store inbs actor → IsBlocked (inbox# ns .name [ IS ] ∷ store) (inb ∷ inbs) actor +is-blocked-suc ns (BlockedReturn at-return no-cont) = BlockedReturn at-return no-cont +is-blocked-suc ns (BlockedReceive at-receive p inbox-for-pointer) = BlockedReceive at-receive (suc {pr = ns .name-is-fresh p} p) (suc inbox-for-pointer) + -- Add a new actor to the environment. -- The actor is added to the top of the list of actors. add-top : ∀ {IS A post} → ActorState ∞ IS A [] post → Env → Env @@ -243,70 +316,115 @@ add-top {IS} {A} {post} m env = record ; blocked-valid = ∀map (valid-actor-suc (env .name-supply .supply)) (blocked-valid env) ; messages-valid = [] ∷ map-suc (store env) (messages-valid env) (env .name-supply .supply) ; name-supply = env .name-supply .next IS + ; blocked-no-progress = ∀map (is-blocked-suc (env .name-supply .supply)) (env .blocked-no-progress) } where + -- ad-hoc ∀map, because we are not using All here map-suc : (store : Store) → {store' : Store} → {inbs : Inboxes store'} → InboxesValid store inbs → (ns : NameSupply store) → InboxesValid (inbox# ns .name [ IS ] ∷ store) inbs map-suc store [] _ = [] map-suc store (x ∷ valid) ns = messages-valid-suc ns x ∷ (map-suc store valid ns) -record GetInbox (store : Store) (S : InboxShape) : Set₂ where + + +record GetInbox (store : Store) {store' : Store} (inboxes : Inboxes store') {name : Name} {S : InboxShape} (p : name ↦ S ∈e store') : Set₂ where field messages : Inbox S valid : all-messages-valid store messages + right-inbox : InboxForPointer messages store' inboxes p + +data InboxState : Set where + Empty NonEmpty : InboxState + +data InboxInState {S : InboxShape} : InboxState → Inbox S → Set₁ where + IsEmpty : InboxInState Empty [] + HasMessage : {nm : NamedMessage S} {rest : Inbox S} → InboxInState NonEmpty (nm ∷ rest) -- Get the messages of an inbox pointed to in the environment. -- This is just a simple lookup into the list of inboxes. -get-inbox : ∀ {name IS} → (env : Env) → name ↦ IS ∈e (store env) → GetInbox (store env) IS +get-inbox : ∀ {name IS} → (env : Env) → (p : name ↦ IS ∈e (store env)) → GetInbox (env .store) (env .env-inboxes) p get-inbox env point = loop (env-inboxes env) (messages-valid env) point where - loop : {store store' : Store} → (inbs : Inboxes store') → InboxesValid store inbs → ∀ {name IS} → name ↦ IS ∈e store' → GetInbox store IS + loop : {store store' : Store} → (inbs : Inboxes store') → InboxesValid store inbs → ∀ {name IS} → (p : name ↦ IS ∈e store') → GetInbox store inbs p loop _ [] () - loop (x ∷ _) (px ∷ _) zero = record { messages = x ; valid = px } - loop (_ ∷ inbs) (_ ∷ valid) (suc point) = loop inbs valid point + loop (x ∷ _) (px ∷ _) zero = record { messages = x ; valid = px ; right-inbox = zero } + loop (_ ∷ inbs) (_ ∷ inb-valid) (suc point) = + let rec = loop inbs inb-valid point + open GetInbox + in record { messages = rec .messages ; valid = rec .valid ; right-inbox = suc (rec .right-inbox) } + +open GetInbox + +record UnblockedActors {store store' : Store} {original : Inboxes store'} {n : Name} (updated : UpdatedInbox store original n) : Set₂ where + field + unblocked : List Actor + unblocked-updated : All (λ act → n ≡ name act) unblocked + unblocked-valid : All (ValidActor store) unblocked + still-blocked : List Actor + blocked-no-prog : All (IsBlocked store' (updated-inboxes updated)) still-blocked + blocked-valid : All (ValidActor store) still-blocked + +open UnblockedActors + +unblock-actors : + {store : Store} → + {original : Inboxes store} → + {n : Name} → + (updated : UpdatedInbox store original n) → + (blocked : List Actor) → + All (ValidActor store) blocked → + All (IsBlocked store original) blocked → + UnblockedActors updated +unblock-actors updated [] [] [] = record + { unblocked = [] + ; unblocked-updated = [] + ; unblocked-valid = [] + ; still-blocked = [] + ; blocked-no-prog = [] + ; blocked-valid = [] + } +unblock-actors {store} {original} {n} updated (x ∷ blckd) (v ∷ blckd-valid) (ib ∷ is-blocked) with (n ≟ (name x)) +... | yes p = + let rec = unblock-actors updated blckd blckd-valid is-blocked + in record + { unblocked = x ∷ rec .unblocked + ; unblocked-updated = p ∷ rec .unblocked-updated + ; unblocked-valid = v ∷ rec .unblocked-valid + ; still-blocked = rec .still-blocked + ; blocked-no-prog = rec .blocked-no-prog + ; blocked-valid = rec .blocked-valid + } +... | no ¬p = + let rec = unblock-actors updated blckd blckd-valid is-blocked + in record + { unblocked = rec .unblocked + ; unblocked-updated = rec .unblocked-updated + ; unblocked-valid = rec .unblocked-valid + ; still-blocked = x ∷ rec .still-blocked + ; blocked-no-prog = blocked-unaffected ib ∷ rec .blocked-no-prog + ; blocked-valid = v ∷ rec .blocked-valid + } + where + blocked-unaffected : IsBlocked store original x → IsBlocked store (updated-inboxes updated) x + blocked-unaffected (BlockedReturn x y) = BlockedReturn x y + blocked-unaffected (BlockedReceive x p y) = BlockedReceive x p (others-unaffected updated ¬p y) --- Updates an inbox in the environment --- Just a wrapper arround 'updateInboxes' update-inbox-env : ∀ {name IS} → (env : Env) → name ↦ IS ∈e (store env) → (f : ValidMessageList (store env) IS → ValidMessageList (store env) IS) → Env -update-inbox-env {name} {IS} env p f = record - { acts = acts env - ; blocked = blocked env - ; env-inboxes = updated-inboxes updated - ; store = store env - ; actors-valid = actors-valid env - ; blocked-valid = blocked-valid env - ; messages-valid = inboxes-valid updated - ; name-supply = env .name-supply - } - where - updated = update-inboxes (store env) (env-inboxes env) (messages-valid env) p f - --- Move an actor from the blocked list to the actors list. --- Simply looks through the names of all blocked actors and moves those (should be just 1 or 0) with the same name. --- IF an actor still doesn't have a way to progress (should never happen), --- it will just get added back to the blocked list the next time it is processed. -unblock-actor : Env → Name → Env -unblock-actor env name = newEnv (loop (blocked env) (blocked-valid env)) - where - loop : (blocked : List Actor) → (blockedValid : All (ValidActor (store env)) blocked) → - (Σ[ blockedAfter ∈ List Actor ] All (ValidActor (store env)) blockedAfter) × (Σ[ unblocked ∈ List Actor ] All (ValidActor (store env)) unblocked) - loop [] [] = ([] , []) , ([] , []) - loop (x ∷ blocked) (px ∷ blockedValid) with (loop blocked blockedValid) - ... | (blockedAfter , baValid) , unblocked , unblockedValid with (Actor.name x ≟ name) - ... | yes p = (blockedAfter , baValid) , ((x ∷ unblocked) , px ∷ unblockedValid) - ... | no ¬p = ((x ∷ blockedAfter) , (px ∷ baValid)) , unblocked , unblockedValid - newEnv : Σ (Σ (List Actor) (All (ValidActor (store env)))) - (λ _ → Σ (List Actor) (All (ValidActor (store env)))) → Env - newEnv ((ba , baValid) , unblocked , unblockedValid) = record - { acts = acts env ++ unblocked - ; blocked = ba - ; env-inboxes = env-inboxes env - ; store = store env - ; actors-valid = ++⁺ (actors-valid env) unblockedValid - ; blocked-valid = baValid - ; messages-valid = messages-valid env - ; name-supply = env .name-supply - } +update-inbox-env {name} {IS} env p f = + let + updated = update-inbox (store env) (env-inboxes env) (messages-valid env) p f + unblock-split = unblock-actors updated (blocked env) (blocked-valid env) (blocked-no-progress env) + in record { + acts = (unblocked unblock-split) ++ acts env + ; blocked = still-blocked unblock-split + ; env-inboxes = updated-inboxes updated + ; store = store env + ; actors-valid = ++⁺ (unblock-split .unblocked-valid) (env .actors-valid) + ; blocked-valid = unblock-split .blocked-valid + ; messages-valid = inboxes-valid updated + ; name-supply = env .name-supply + ; blocked-no-progress = unblock-split .blocked-no-prog + } record FoundReference (store : Store) (S : InboxShape) : Set₂ where field @@ -324,6 +442,8 @@ lookup-reference _ (_ ∷ refs) (_ ∷ prfs) refl (S px) = lookup-reference _ re lookup-reference-act : ∀ {store actor ToIS} → ValidActor store actor → ToIS ∈ (pre actor) → FoundReference store ToIS lookup-reference-act {store} {actor} {ToIS} va ref = lookup-reference (pre actor) (Actor.references actor) (ValidActor.references-have-pointer va) (pre-eq-refs actor) ref + + open _comp↦_∈_ open FoundReference @@ -342,25 +462,25 @@ record LiftedReferences (lss gss : TypingContext) (references : List NamedInbox) subset-inbox : lss ⊆ gss contained : List NamedInbox subset : contained ⊆ references - contained-eq-inboxes : lss ≡ map shape contained + contained-eq-inboxes : map shape contained ≡ lss open LiftedReferences -- Convert a subset for preconditions to a subset for references lift-references : ∀ {lss gss} → lss ⊆ gss → (references : List NamedInbox) → map shape references ≡ gss → LiftedReferences lss gss references -lift-references [] refs refl = record - { subset-inbox = [] - ; contained = [] - ; subset = [] - ; contained-eq-inboxes = refl - } +lift-references [] refs refl = record { + subset-inbox = [] + ; contained = [] + ; subset = [] + ; contained-eq-inboxes = refl + } lift-references (_∷_ {y} {xs} x₁ subs) refs refl with (lift-references subs refs refl) -... | q = record - { subset-inbox = x₁ ∷ subs - ; contained = (lookup-parallel x₁ refs shape refl) ∷ contained q - ; subset = (translate-∈ x₁ refs shape refl) ∷ (subset q) - ; contained-eq-inboxes = combine y (shape (lookup-parallel x₁ refs shape refl)) xs (map shape (contained q)) contained-el-ok (contained-eq-inboxes q) - } +... | q = record { + subset-inbox = x₁ ∷ subs + ; contained = contained-el ∷ contained q + ; subset = (translate-∈ x₁ refs shape refl) ∷ (subset q) + ; contained-eq-inboxes = combine contained-el-shape y (map shape (contained q)) xs (sym contained-el-ok) (contained-eq-inboxes q) + } where contained-el : NamedInbox contained-el = lookup-parallel x₁ refs shape refl @@ -370,32 +490,88 @@ lift-references (_∷_ {y} {xs} x₁ subs) refs refl with (lift-references subs combine : (a b : InboxShape) → (as bs : TypingContext) → (a ≡ b) → (as ≡ bs) → (a ∷ as ≡ b ∷ bs) combine a .a as .as refl refl = refl +data LiftActor : Actor → Actor → Set₂ where + CanBeLifted : + ∀ {A A' post post'} + {IS name references} + {lss gss} + {per} + {computation computation'} → + (lr : LiftedReferences lss gss references) → + LiftActor + (record + { inbox-shape = IS + ; A = A + ; references = references + ; pre = gss + ; pre-eq-refs = per + ; post = post + ; computation = computation + ; name = name + }) + (record + { inbox-shape = IS + ; A = A' + ; references = lr .contained + ; pre = lss + ; pre-eq-refs = lr .contained-eq-inboxes + ; post = post' + ; computation = computation' + ; name = name + }) + +lift-valid-actor : ∀ {store} {act act' : Actor} → + LiftActor act act' → + ValidActor store act → + ValidActor store act' +lift-valid-actor (CanBeLifted lr) va = + record { + actor-has-inbox = va .actor-has-inbox + ; references-have-pointer = All-⊆ (lr .subset) (va .references-have-pointer) + } + + + -- We can replace the actors in an environment if they all are valid for the current store. replace-actors : (env : Env) → (actors : List Actor) → All (ValidActor (store env)) actors → Env replace-actors env actors actorsValid = record { acts = actors - ; blocked = blocked env - ; env-inboxes = env-inboxes env - ; store = store env + ; blocked = env .blocked + ; env-inboxes = env .env-inboxes + ; store = env .store ; actors-valid = actorsValid - ; blocked-valid = blocked-valid env - ; messages-valid = messages-valid env + ; blocked-valid = env .blocked-valid + ; messages-valid = env .messages-valid ; name-supply = env .name-supply + ; blocked-no-progress = env .blocked-no-progress } --- We can replace both the running and blocked actors in an environment if they all are valid for the current store. -replace-actors+blocked : (env : Env) → - (actors : List Actor) → All (ValidActor (store env)) actors → - (blocked : List Actor) → All (ValidActor (store env)) blocked → Env -replace-actors+blocked env actors actorsValid blocked blockedValid = record { - acts = actors +replace-focused : {act : Actor} → (env : Env) → Focus act env → + (act' : Actor) → + (valid' : ValidActor (env .store) act') → + Env +replace-focused env@record { + acts = _ ∷ rest + ; actors-valid = _ ∷ rest-valid + } Focused act' valid' = + replace-actors env (act' ∷ rest) (valid' ∷ rest-valid) + +block-focused : {act : Actor} → (env : Env) → Focus act env → IsBlocked (env .store) (env .env-inboxes) act → Env +block-focused env@record { + acts = actor ∷ rest ; blocked = blocked - ; env-inboxes = env-inboxes env - ; store = store env - ; actors-valid = actorsValid - ; blocked-valid = blockedValid - ; messages-valid = messages-valid env + ; actors-valid = actor-valid ∷ rest-valid + ; blocked-valid = blocked-valid + } Focused blckd = record { + acts = rest + ; blocked = actor ∷ blocked + ; store = env .store + ; env-inboxes = env .env-inboxes ; name-supply = env .name-supply + ; actors-valid = rest-valid + ; blocked-valid = actor-valid ∷ blocked-valid + ; messages-valid = env .messages-valid + ; blocked-no-progress = blckd ∷ env .blocked-no-progress } -- Takes a named message and a proof that the named message is valid for the store. @@ -427,14 +603,6 @@ unname-field : ∀ {x} → named-field-content x → receive-field-content x unname-field {ValueType x₁} nfc = nfc unname-field {ReferenceType x₁} nfc = _ -unname-message : ∀ {S} → NamedMessage S → Message S -unname-message (NamedM x fields) = Msg x (do-the-work fields) - where - do-the-work : ∀ {MT} → All named-field-content MT → All receive-field-content MT - do-the-work {[]} nfc = [] - do-the-work {ValueType x₁ ∷ MT} (px ∷ nfc) = px ∷ (do-the-work nfc) - do-the-work {ReferenceType x₁ ∷ MT} (px ∷ nfc) = _ ∷ do-the-work nfc - extract-inboxes : ∀ {MT} → All named-field-content MT → List NamedInbox extract-inboxes [] = [] extract-inboxes (_∷_ {ValueType _} _ ps) = extract-inboxes ps @@ -482,9 +650,10 @@ compatible-handles : ∀ store x refs (px : (map shape refs) ⊢>: x) (w : FoundReference store (actual px)) → x ⊆ actual (reference w) -compatible-handles store x refs px w with (actual-handles-requested px) -... | a with (actual-handles-wanted (reference w)) -... | b = ⊆-trans a b +compatible-handles store x refs px w = + let a = actual-handles-requested px + b = actual-handles-wanted (reference w) + in ⊆-trans a b make-pointer-compatible : ∀ store x refs (px : (map shape refs) ⊢>: x) → @@ -501,8 +670,6 @@ make-pointers-compatible : ∀ {MT} store pre refs (eq : map shape refs ≡ pre) FieldsHavePointer store (name-fields pre refs rhp fields eq) make-pointers-compatible store pre refs eq [] rhp = [] make-pointers-compatible store _ refs refl (_∷_ {ValueType x} px fields) rhp = FhpV ∷ make-pointers-compatible store _ refs refl fields rhp -make-pointers-compatible store _ refs refl (_∷_ {ReferenceType x} px fields) rhp = FhpR (make-pointer-compatible store x refs px rhp foundFw) ∷ (make-pointers-compatible store _ refs refl fields rhp) - where - foundFw : FoundReference store (actual px) - foundFw = lookup-reference _ refs rhp refl (actual-is-sendable px) - +make-pointers-compatible store _ refs refl (_∷_ {ReferenceType x} px fields) rhp = + let foundFw = lookup-reference _ refs rhp refl (actual-is-sendable px) + in FhpR (make-pointer-compatible store x refs px rhp foundFw) ∷ (make-pointers-compatible store _ refs refl fields rhp) diff --git a/src/Examples/Call.lagda.tex b/src/Examples/Call.lagda.tex index 77440aa..782b477 100644 --- a/src/Examples/Call.lagda.tex +++ b/src/Examples/Call.lagda.tex @@ -13,11 +13,12 @@ using (_≡_ ; refl ; cong ; sym ; inspect ; [_] ; trans) open import Membership using ( _∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] ; ⊆-refl - ; ⊆-trans ; ⊆-suc ; translate-⊆) + ; ⊆-trans ; ⊆-suc ; translate-⊆ + ; ∈-inc ; ⊆++-refl) open import Data.Unit using (⊤ ; tt) open import Examples.SelectiveReceive using ( selective-receive ; SelRec ; waiting-refs - ; add-references++ ; ∈-inc ; ⊆++-refl) + ; add-references++) open import Relation.Nullary using (yes ; no) open import Size @@ -116,4 +117,4 @@ return-result record { msg = (Msg Z (tag ∷ n ∷ [])) } = return n return-result record { msg = (Msg (S x) x₁) ; msg-ok = () } -\end{code} \ No newline at end of file +\end{code} diff --git a/src/Examples/Main-template.agda b/src/Examples/Main-template.agda index e9b752c..dd70fb0 100644 --- a/src/Examples/Main-template.agda +++ b/src/Examples/Main-template.agda @@ -14,4 +14,4 @@ infinitebindEntry = singleton-env (InfiniteBind.binder .force) selectiveReceiveEntry = singleton-env SelectiveReceive.spawner callEntry = singleton-env (Call.calltestActor .force) -main = IO.run (run-env trace+actors-logger __ENTRY__) +main = IO.run (run-env __ENTRY__) diff --git a/src/Examples/Main.agda b/src/Examples/Main.agda index 11a55fa..dcbc425 100644 --- a/src/Examples/Main.agda +++ b/src/Examples/Main.agda @@ -14,4 +14,4 @@ infinitebindEntry = singleton-env (InfiniteBind.binder .force) selectiveReceiveEntry = singleton-env SelectiveReceive.spawner callEntry = singleton-env (Call.calltestActor .force) -main = IO.run (run-env trace+actors-logger pingpongEntry) +main = IO.run (run-env pingpongEntry) diff --git a/src/Examples/SelectiveReceive.lagda.tex b/src/Examples/SelectiveReceive.lagda.tex index cc54805..c92c736 100644 --- a/src/Examples/SelectiveReceive.lagda.tex +++ b/src/Examples/SelectiveReceive.lagda.tex @@ -15,7 +15,6 @@ open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong ; sym ; inspect ; [_] ; trans) open import Membership - using (_∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] ; ⊆-refl ; ⊆-trans ; ⊆-suc) open import Data.Unit using (⊤ ; tt) @@ -60,94 +59,6 @@ ; is-ls = refl }) eq -⊆++ : {a : Level} {A : Set a} - (xs ys zs : List A) → - xs ⊆ zs → ys ⊆ zs → - (xs ++ ys) ⊆ zs -⊆++ _ ys zs [] q = q -⊆++ _ ys zs (x₁ ∷ p) q = x₁ ∷ (⊆++ _ ys zs p q) - -∈-insert : ∀ {a} {A : Set a} - (xs ys : List A) → - (x : A) → - x ∈ (ys ++ x ∷ xs) -∈-insert xs [] x = Z -∈-insert xs (x₁ ∷ ys) x = S (∈-insert xs ys x) - --- count down both the proof and the list --- Result depends on which is shortest -insert-one : ∀ {a} {A : Set a} {x₁ : A} - (xs ys : List A) → - (y : A) → - x₁ ∈ (xs ++ ys) → - x₁ ∈ (xs ++ y ∷ ys) -insert-one [] ys y p = S p -insert-one (x ∷ xs) ys y Z = Z -insert-one (x ∷ xs) ys y (S p) = S (insert-one xs ys y p) - -⊆-insert : ∀ {a} {A : Set a} - (xs ys zs : List A) → - (x : A) → - xs ⊆ (ys ++ zs) → - xs ⊆ (ys ++ x ∷ zs) -⊆-insert [] ys zs x p = [] -⊆-insert (x₁ ∷ xs) ys zs x (x₂ ∷ p) = insert-one ys zs x x₂ ∷ - (⊆-insert xs ys zs x p) - -⊆-move : {a : Level} {A : Set a} - (xs ys : List A) → - (xs ++ ys) ⊆ (ys ++ xs) -⊆-move [] ys rewrite (++-identityʳ ys) = ⊆-refl -⊆-move (x ∷ xs) ys with (⊆-move xs ys) -... | q = ∈-insert xs ys x ∷ ⊆-insert (xs ++ ys) ys xs x q - -⊆-skip : {a : Level} {A : Set a} - (xs ys zs : List A) → - ys ⊆ zs → - (xs ++ ys) ⊆ (xs ++ zs) -⊆-skip [] ys zs p = p -⊆-skip (x ∷ xs) ys zs p = Z ∷ (⊆-suc (⊆-skip xs ys zs p)) - -⊆++-refl : ∀ {a} {A : Set a} → - (xs ys : List A) → - xs ⊆ (xs ++ ys) -⊆++-refl [] ys = [] -⊆++-refl (x ∷ xs) ys = Z ∷ (⊆-suc (⊆++-refl xs ys)) - -⊆++-l-refl : ∀ {a} {A : Set a} → - (xs ys : List A) → - xs ⊆ (ys ++ xs) -⊆++-l-refl xs [] = ⊆-refl -⊆++-l-refl xs (x ∷ ys) = ⊆-suc (⊆++-l-refl xs ys) - -∈-inc : ∀ {a} {A : Set a} - (xs ys : List A) → - (x : A) → - x ∈ xs → - x ∈ (xs ++ ys) -∈-inc _ ys x Z = Z -∈-inc _ ys x (S p) = S (∈-inc _ ys x p) - -⊆-inc : ∀ {a} {A : Set a} - (xs ys zs : List A) → - xs ⊆ ys → - (xs ++ zs) ⊆ (ys ++ zs) -⊆-inc [] [] zs p = ⊆-refl -⊆-inc [] (x ∷ ys) zs p = ⊆++-l-refl zs (x ∷ ys) -⊆-inc (x ∷ xs) ys zs (px ∷ p) = ∈-inc ys zs x px ∷ (⊆-inc xs ys zs p) - -⊆++comm : ∀ {a} {A : Set a} - (xs ys zs : List A) → - ((xs ++ ys) ++ zs) ⊆ (xs ++ (ys ++ zs)) -⊆++comm [] ys zs = ⊆-refl -⊆++comm (x ∷ xs) ys zs = Z ∷ (⊆-suc (⊆++comm xs ys zs)) - -⊆++comm' : ∀ {a} {A : Set a} - (xs ys zs : List A) → - (xs ++ ys ++ zs) ⊆ ((xs ++ ys) ++ zs) -⊆++comm' [] ys zs = ⊆-refl -⊆++comm' (x ∷ xs) ys zs = Z ∷ ⊆-suc (⊆++comm' xs ys zs) - add-references++ : ∀ {IS} → (xs ys : ReferenceTypes) → (x : Message IS) → add-references (xs ++ ys) x ≡ @@ -346,6 +257,6 @@ spawner : ∀ {i} → ActorM i [] ⊤₁ [] (λ _ → []) spawner = spawn testActor ∞>> - ((Z ![t: Z ] ((lift false) ∷ [])) >> + ((Z ![t: Z ] ((lift true) ∷ [])) >> strengthen []) \end{code} diff --git a/src/Membership.lagda.tex b/src/Membership.lagda.tex index 47fc908..74012a7 100644 --- a/src/Membership.lagda.tex +++ b/src/Membership.lagda.tex @@ -5,8 +5,10 @@ open import Data.List open import Data.List.Any using () open import Data.List.All using (All ; [] ; _∷_) +open import Data.List.Properties using (++-assoc ; ++-identityʳ) open import Relation.Binary.PropositionalEquality using (_≡_ ; refl) open import Data.Empty using (⊥) +open import Level using (Level) renaming (zero to lzero ; suc to lsuc) \end{code} %<*ElementIn> \begin{code} @@ -78,4 +80,116 @@ ⊆-trans : ∀ {a} {A : Set a} {as bs cs : List A} → as ⊆ bs → bs ⊆ cs → as ⊆ cs ⊆-trans [] _ = [] ⊆-trans (x₁ ∷ asbs) bscs = (translate-⊆ bscs x₁) ∷ (⊆-trans asbs bscs) + + +⊆++ : {a : Level} {A : Set a} + (xs ys zs : List A) → + xs ⊆ zs → ys ⊆ zs → + (xs ++ ys) ⊆ zs +⊆++ _ ys zs [] q = q +⊆++ _ ys zs (x₁ ∷ p) q = x₁ ∷ (⊆++ _ ys zs p q) + +∈-insert : ∀ {a} {A : Set a} + (xs ys : List A) → + (x : A) → + x ∈ (ys ++ x ∷ xs) +∈-insert xs [] x = Z +∈-insert xs (x₁ ∷ ys) x = S (∈-insert xs ys x) + +-- count down both the proof and the list +-- Result depends on which is shortest +insert-one : ∀ {a} {A : Set a} {x₁ : A} + (xs ys : List A) → + (y : A) → + x₁ ∈ (xs ++ ys) → + x₁ ∈ (xs ++ y ∷ ys) +insert-one [] ys y p = S p +insert-one (x ∷ xs) ys y Z = Z +insert-one (x ∷ xs) ys y (S p) = S (insert-one xs ys y p) + +⊆-insert : ∀ {a} {A : Set a} + (xs ys zs : List A) → + (x : A) → + xs ⊆ (ys ++ zs) → + xs ⊆ (ys ++ x ∷ zs) +⊆-insert [] ys zs x p = [] +⊆-insert (x₁ ∷ xs) ys zs x (x₂ ∷ p) = insert-one ys zs x x₂ ∷ + (⊆-insert xs ys zs x p) + +⊆-move : {a : Level} {A : Set a} + (xs ys : List A) → + (xs ++ ys) ⊆ (ys ++ xs) +⊆-move [] ys rewrite (++-identityʳ ys) = ⊆-refl +⊆-move (x ∷ xs) ys with (⊆-move xs ys) +... | q = ∈-insert xs ys x ∷ ⊆-insert (xs ++ ys) ys xs x q + +⊆-skip : {a : Level} {A : Set a} + (xs ys zs : List A) → + ys ⊆ zs → + (xs ++ ys) ⊆ (xs ++ zs) +⊆-skip [] ys zs p = p +⊆-skip (x ∷ xs) ys zs p = Z ∷ (⊆-suc (⊆-skip xs ys zs p)) + +⊆++-refl : ∀ {a} {A : Set a} → + (xs ys : List A) → + xs ⊆ (xs ++ ys) +⊆++-refl [] ys = [] +⊆++-refl (x ∷ xs) ys = Z ∷ (⊆-suc (⊆++-refl xs ys)) + +⊆++-l-refl : ∀ {a} {A : Set a} → + (xs ys : List A) → + xs ⊆ (ys ++ xs) +⊆++-l-refl xs [] = ⊆-refl +⊆++-l-refl xs (x ∷ ys) = ⊆-suc (⊆++-l-refl xs ys) + +∈-inc : ∀ {a} {A : Set a} + (xs ys : List A) → + (x : A) → + x ∈ xs → + x ∈ (xs ++ ys) +∈-inc _ ys x Z = Z +∈-inc _ ys x (S p) = S (∈-inc _ ys x p) + +⊆-inc : ∀ {a} {A : Set a} + (xs ys zs : List A) → + xs ⊆ ys → + (xs ++ zs) ⊆ (ys ++ zs) +⊆-inc [] [] zs p = ⊆-refl +⊆-inc [] (x ∷ ys) zs p = ⊆++-l-refl zs (x ∷ ys) +⊆-inc (x ∷ xs) ys zs (px ∷ p) = ∈-inc ys zs x px ∷ (⊆-inc xs ys zs p) + +⊆++comm : ∀ {a} {A : Set a} + (xs ys zs : List A) → + ((xs ++ ys) ++ zs) ⊆ (xs ++ (ys ++ zs)) +⊆++comm [] ys zs = ⊆-refl +⊆++comm (x ∷ xs) ys zs = Z ∷ (⊆-suc (⊆++comm xs ys zs)) + +⊆++comm' : ∀ {a} {A : Set a} + (xs ys zs : List A) → + (xs ++ ys ++ zs) ⊆ ((xs ++ ys) ++ zs) +⊆++comm' [] ys zs = ⊆-refl +⊆++comm' (x ∷ xs) ys zs = Z ∷ ⊆-suc (⊆++comm' xs ys zs) + +pad-pointer : ∀ {a} {A : Set a} → (l r : List A) → {v : A} → v ∈ r → v ∈ (l ++ r) +pad-pointer [] r p = p +pad-pointer (x ∷ l) r p = S (pad-pointer l r p) + +record ElemInList {a} {A : Set a} (ls : List A) : Set a where + field + elem : A + in-list : elem ∈ ls + +tabulate-suc : ∀ {a} {A : Set a} → {ls : List A} → {x : A} → List (ElemInList ls) → List (ElemInList (x ∷ ls)) +tabulate-suc [] = [] +tabulate-suc (eil ∷ tabs) = + let rec = tabulate-suc tabs + open ElemInList + in record { elem = eil .elem ; in-list = S (eil .in-list) } ∷ rec + +tabulate-∈ : ∀ {a} {A : Set a} → (ls : List A) → List (ElemInList ls) +tabulate-∈ [] = [] +tabulate-∈ (x ∷ ls) = + let rec = tabulate-∈ ls + in record { elem = x ; in-list = Z } ∷ tabulate-suc rec + \end{code} diff --git a/src/NatProps.agda b/src/NatProps.agda new file mode 100644 index 0000000..ab84cbc --- /dev/null +++ b/src/NatProps.agda @@ -0,0 +1,13 @@ +module NatProps where +open import Data.Nat using (ℕ ; _≟_ ; _<_ ; zero ; suc ; s≤s) +open import Data.Nat.Properties using (s≤s-injective) +open import Relation.Nullary using (Dec ; yes ; no ; ¬_) +open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym) +open import Data.Empty using (⊥) + +<-¬≡ : ∀ {n m} → n < m → ¬ n ≡ m +<-¬≡ {zero} {zero} () +<-¬≡ {zero} {suc m} p = λ () +<-¬≡ {suc n} {zero} p = λ () +<-¬≡ {suc n} {suc m} (Data.Nat.s≤s p) with (<-¬≡ p) +... | q = λ { refl → q refl } diff --git a/src/Runtime.agda b/src/Runtime.agda index a295c04..01762f5 100644 --- a/src/Runtime.agda +++ b/src/Runtime.agda @@ -2,8 +2,8 @@ module Runtime where open import Simulate open import SimulationEnvironment -open import Colist using (Colist ; ∞Colist ; [] ; _∷_) open import Data.List using (List ; _∷_ ; [] ; map ; length) +open import Data.List.All using (All ; _∷_ ; []) open import Data.Nat using (ℕ ; zero ; suc) open import Data.Nat.Show using (show) open import Data.String using (String ; _++_) @@ -12,76 +12,54 @@ open import Data.Unit using (⊤ ; tt) open import Coinduction using ( ♯_ ; ♭) open import Size using (∞) import IO -open ∞Colist +open ∞Trace -Logger = (ℕ → EnvStep → IO.IO ⊤) +record BlockedCount : Set₂ where + field + return-count : ℕ + receive-count : ℕ + +count-blocked : (env : Env) → BlockedCount +count-blocked env = loop (Env.blocked-no-progress env) + where + open BlockedCount + loop : ∀ {store inbs bl} → All (IsBlocked store inbs) bl → BlockedCount + loop [] = record { return-count = 0 ; receive-count = 0 } + loop (BlockedReturn _ _ ∷ xs) = + let rec = loop xs + in record { return-count = suc (rec .return-count) ; receive-count = rec .receive-count } + loop (BlockedReceive _ _ _ ∷ xs) = + let rec = loop xs + in record { return-count = rec .return-count ; receive-count = suc (rec .receive-count) } + +show-env : Env → String +show-env env = + let count = count-blocked env + open BlockedCount + in "There are " ++ show (count .return-count) ++ " finished actors and " ++ show (count .receive-count) ++ " blocked actors" + +show-final-step : ℕ → String +show-final-step n = "Done after " ++ (show n) ++ " steps." -- run-env continously runs the simulation of an environment -- and transforms the steps taken into output to the console. --- The output can be configured by prodiving different loggers. -run-env : Logger → Env → IO.IO ⊤ -run-env logger env = loop 1 ((simulate env) .force) +run-env : Env → IO.IO ⊤ +run-env env = loop 1 ((simulate env) .force) where - loop : ℕ → Colist ∞ EnvStep → IO.IO ⊤ - loop n [] = IO.putStrLn ("Done after " ++ (show n) ++ " steps.") - loop n (x ∷ xs) = ♯ logger n x IO.>> ♯ loop (suc n) (xs .force) - -open EnvStep -open Env - -showNames : List Name → String -showNames [] = "" -showNames (x ∷ []) = show x -showNames (x ∷ x₁ ∷ names) = show x ++ ", " ++ showNames (x₁ ∷ names) - --- Creates a nicely formatted string out of a step-trace from the simulation -show-trace : Trace → String -show-trace (Return name) = show name ++ " returned" -show-trace (Bind name) = "Bind [ " ++ show name ++ " ]" -show-trace (Spawn spawner spawned) = (show spawner) ++ " spawned " ++ (show spawned) -show-trace (Send sender receiver references) = (show sender) ++ " sent a message to " ++ (show receiver) ++ " forwarding [" ++ showNames references ++ "]" -show-trace (Receive name Nothing) = (show name) ++ " received nothing. It was put in the blocked list" -show-trace (Receive name (Value references)) = (show name) ++ " received a message forwarding [" ++ showNames references ++ "]" -show-trace (Receive name Dropped) = (show name) ++ " received something, but had no bind. It was dropped" -show-trace (Strengthen name) = (show name) ++ " was strengthened" -show-trace (Self name) = (show name ++ " used self") - --- Output the string of the trace for this step -log-trace : Trace → IO.IO ⊤ -log-trace trace = IO.putStrLn (show-trace trace ++ ".") - --- Output the number of inboxes in the environment. -log-inbox-count : ∀ {store} → Inboxes store → IO.IO ⊤ -log-inbox-count {store} inboxes = IO.putStrLn ("There are " ++ (show (Data.List.length store)) ++ " inboxes.") - --- Output the number of messages in an inbox -log-message-counts : ∀ {store} → Inboxes store → IO.IO ⊤ -log-message-counts [] = IO.return _ -log-message-counts {inbox# name [ _ ] ∷ store} (x ∷ xs) = ♯ IO.putStrLn ("Inbox #" ++ show name ++ " has " ++ (show (Data.List.length x)) ++ " messages.") IO.>> ♯ log-message-counts xs + loop : ℕ → Trace ∞ → IO.IO ⊤ + loop n (TraceStop env _) = ♯ IO.putStrLn (show-final-step n) IO.>> ♯ IO.putStrLn (show-env env) + loop n (x ∷ xs) = ♯ IO.putStrLn ("Step " ++ show n ) IO.>> ♯ loop (suc n) (xs .force) --- Output the nunmber of inboxes and how many messages are in each inbox. -log-inboxes : ∀ {store} → Inboxes store → IO.IO ⊤ -log-inboxes inboxes = ♯ log-inbox-count inboxes IO.>> ♯ log-message-counts inboxes - --- Output how many actors are currently running and how many actors are blocked. -log-actors+blocked : Env → IO.IO ⊤ -log-actors+blocked env = IO.putStrLn ("[A : " ++ show (length (acts env)) ++ " , B : " ++ show (length (blocked env)) ++ "]") - --- Count the number of steps taken -count-logger : Logger -count-logger n step = IO.putStrLn ((show n)) - -trace-logger : Logger -trace-logger n step = log-trace (trace step) - -trace+inbox-logger : Logger -trace+inbox-logger n step = ♯ trace-logger n step IO.>> ♯ log-inboxes (env-inboxes (env step)) - -count+trace+inbox-logger : Logger -count+trace+inbox-logger n step = ♯ count-logger n step IO.>> ♯ trace+inbox-logger n step - -actors-logger : Logger -actors-logger n step = log-actors+blocked (env step) +run-env-silent : Env → IO.IO ⊤ +run-env-silent env = loop 1 ((simulate env) .force) + where + loop : ℕ → Trace ∞ → IO.IO ⊤ + loop n (TraceStop env _) = IO.putStrLn (show-final-step n) + loop n (x ∷ xs) = ♯ IO.return tt IO.>> ♯ loop (suc n) (xs .force) -trace+actors-logger : Logger -trace+actors-logger n step = ♯ trace-logger n step IO.>> ♯ actors-logger n step +run-env-end : Env → IO.IO Env +run-env-end env = loop ((simulate env) .force) + where + loop : Trace ∞ → IO.IO Env + loop (TraceStop env _) = IO.return env + loop (x ∷ xs) = ♯ IO.return x IO.>> ♯ loop (xs .force) diff --git a/src/Selective/ActorMonad.lagda.tex b/src/Selective/ActorMonad.lagda.tex index ec6cfd3..35312b0 100644 --- a/src/Selective/ActorMonad.lagda.tex +++ b/src/Selective/ActorMonad.lagda.tex @@ -39,23 +39,36 @@ send-field-content Γ (ValueType A) = Lift A send-field-content Γ (ReferenceType requested) = Γ ⊢>: requested -data SendMessage (To : InboxShape) (Γ : TypingContext) : Set₁ where - SendM : {MT : MessageType} → MT ∈ To → All (send-field-content Γ) MT → SendMessage To Γ +record SendMessage (To : InboxShape) (Γ : TypingContext) : Set₁ where + constructor SendM + field + {MT} : MessageType + selected-message-type : MT ∈ To + send-fields : All (send-field-content Γ) MT receive-field-content : MessageField → Set receive-field-content (ValueType A) = A receive-field-content (ReferenceType Fw) = ⊤ -data Message (To : InboxShape) : Set₁ where - Msg : {MT : MessageType} → MT ∈ To → All receive-field-content MT → Message To +record Message (To : InboxShape) : Set₁ where + constructor Msg + field + {MT} : MessageType + received-message-type : MT ∈ To + received-fields : All receive-field-content MT extract-references : MessageType → ReferenceTypes extract-references [] = [] extract-references (ValueType x ∷ mt) = extract-references mt extract-references (ReferenceType T ∷ mt) = T ∷ extract-references mt +add-references-static : TypingContext → MessageType → TypingContext +add-references-static Γ MT = extract-references MT ++ Γ + add-references : ∀ {To} → TypingContext → Message To → TypingContext -add-references Γ (Msg {MT} x x₁) = extract-references MT ++ Γ +add-references Γ msg = + let open Message + in add-references-static Γ (msg .MT) \end{code} %<*MessageFilter> @@ -77,16 +90,24 @@ %<*SelectedMessageAddReferences> \begin{code} + +selected-type : ∀ {IS} + {filter : MessageFilter IS} → + SelectedMessage filter → + MessageType +selected-type record {msg = msg } = + let open Message + in msg .MT + add-selected-references : TypingContext → ∀ {IS} {filter : MessageFilter IS} → SelectedMessage filter → TypingContext -add-selected-references Γ m = - add-references Γ (SelectedMessage.msg m) +add-selected-references Γ m = add-references-static Γ (selected-type m) \end{code} % \begin{code} - + ⊤₁ : Set₁ ⊤₁ = Lift ⊤ @@ -184,13 +205,20 @@ ∞ActorM (↑ i) IS ⊤₁ pre λ _ → NewIS ∷ pre spawn∞ newAct = spawn (newAct .force) + +send : ∀ {i IS ToIS pre} → + (canSendTo : ToIS ∈ pre) → + (SendMessage ToIS pre) → + ∞ActorM (↑ i) IS ⊤₁ pre (λ _ → pre) +send p m .force = Send p m + -- coinduction helper and neater syntax for message sending _![t:_]_ : ∀ {i IS ToIS pre MT} → (canSendTo : ToIS ∈ pre) → (MT ∈ ToIS) → All (send-field-content pre) MT → ∞ActorM (↑ i) IS ⊤₁ pre (λ _ → pre) -(canSendTo ![t: p ] fields) .force = Send canSendTo (SendM p fields) +(canSendTo ![t: p ] fields) = send canSendTo (SendM p fields) -- coinduction helper for Receive receive : ∀ {i IS pre} → ∞ActorM (↑ i) IS (Message IS) pre (add-references pre) @@ -207,6 +235,9 @@ strengthen : ∀ {i IS xs ys} → ys ⊆ xs → ∞ActorM (↑ i) IS ⊤₁ xs (λ _ → ys) strengthen inc .force = Strengthen inc +begin : ∀ {i IS A pre post} → ∞ActorM i IS A pre post → ActorM i IS A pre post +begin = _∞>>_ (return tt) + ⊠-of-values : List Set → InboxShape ⊠-of-values [] = [] ⊠-of-values (x ∷ vs) = (ValueType x ∷ []) ∷ ⊠-of-values vs diff --git a/src/Selective/EnvironmentOperations.agda b/src/Selective/EnvironmentOperations.agda index f55cbcb..f99d3a7 100644 --- a/src/Selective/EnvironmentOperations.agda +++ b/src/Selective/EnvironmentOperations.agda @@ -1,7 +1,7 @@ module Selective.EnvironmentOperations where open import Selective.ActorMonad open import Selective.SimulationEnvironment -open import Membership using (_∈_ ; _⊆_ ; [] ; _∷_ ; Z ; S ; lookup-parallel ; lookup-parallel-≡ ; translate-∈ ; x∈[]-⊥ ; translate-⊆ ; ⊆-trans ; find-∈) +open import Membership using (_∈_ ; _⊆_ ; [] ; _∷_ ; Z ; S ; lookup-parallel ; lookup-parallel-≡ ; translate-∈ ; x∈[]-⊥ ; translate-⊆ ; ⊆-trans ; find-∈ ; All-⊆) open import Data.List using (List ; _∷_ ; [] ; map ; _++_ ; drop) open import Data.List.All using (All ; _∷_ ; []; lookup) renaming (map to ∀map) @@ -16,9 +16,9 @@ open import Data.Empty using (⊥ ; ⊥-elim) open import Data.Bool using (Bool ; true ; false) open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; cong ; cong₂ ; trans ; inspect ; [_]) -open import Relation.Nullary using (Dec ; yes ; no) +open import Relation.Nullary using (Dec ; yes ; no ; ¬_) -open import Level using (Level ; Lift ; lift) renaming (suc to lsuc) +open import Level using (Lift ; lift) open import Size using (∞) open Actor @@ -50,13 +50,13 @@ lift-actor : (actor : Actor) → {pre : TypingContext} → Actor lift-actor actor {pre} references pre-eq-refs m = record { inbox-shape = inbox-shape actor - ; A = A actor + ; A = actor .A ; references = references ; pre = pre ; pre-eq-refs = pre-eq-refs - ; post = post actor + ; post = actor .post ; computation = m - ; name = name actor + ; name = actor .name } -- Replace the monadic part of an actor @@ -115,31 +115,97 @@ add-references-rewrite actor nms {x} p m = record ; name = name actor } +data SameValidityProof : Actor → Actor → Set₁ where + AreSame : + ∀ {A A' pre pre' post post'} + {IS name references} + {per per'} + {computation computation'} → + SameValidityProof + (record + { inbox-shape = IS + ; A = A + ; references = references + ; pre = pre + ; pre-eq-refs = per + ; post = post + ; computation = computation + ; name = name + }) + (record + { inbox-shape = IS + ; A = A' + ; references = references + ; pre = pre' + ; pre-eq-refs = per' + ; post = post' + ; computation = computation' + ; name = name + }) + -- A proof of an actor being valid is also valid for another actor if -- * they have the same name -- * they have the same references -- * they have the same inbox type rewrap-valid-actor : {store : Store} → {actorPre : Actor} → {actorPost : Actor} → + SameValidityProof actorPre actorPost → ValidActor store actorPre → - (name actorPre) ≡ (name actorPost) → - (references actorPre) ≡ (references actorPost) → - (inbox-shape actorPre) ≡ (inbox-shape actorPost) → ValidActor store actorPost -rewrap-valid-actor va refl refl refl = record { actor-has-inbox = actor-has-inbox va - ; references-have-pointer = references-have-pointer va } +rewrap-valid-actor AreSame va = record { actor-has-inbox = va .actor-has-inbox ; references-have-pointer = va .references-have-pointer } + +data ReferenceAdded (ref : NamedInbox) : Actor → Actor → Set₁ where + RefAdded : + ∀ {A A' pre pre' post post'} + {IS name references} + {per per'} + {computation computation'} → + ReferenceAdded ref + (record + { inbox-shape = IS + ; A = A + ; references = references + ; pre = pre + ; pre-eq-refs = per + ; post = post + ; computation = computation + ; name = name + }) + (record + { inbox-shape = IS + ; A = A' + ; references = ref ∷ references + ; pre = pre' + ; pre-eq-refs = per' + ; post = post' + ; computation = computation' + ; name = name + }) + +add-reference-valid : {store : Store} → {actorPre : Actor} → {actorPost : Actor} → + {ref : NamedInbox} → + ReferenceAdded ref actorPre actorPost → + ValidActor store actorPre → + reference-has-pointer store ref → + ValidActor store actorPost +add-reference-valid RefAdded va p = record { actor-has-inbox = va .actor-has-inbox ; references-have-pointer = p ∷ (va .references-have-pointer) } record ValidMessageList (store : Store) (S : InboxShape) : Set₁ where field inbox : Inbox S valid : All (message-valid store) inbox -record UpdatedInboxes (store : Store) {store' : Store} (original : Inboxes store') : Set₂ where +InboxUpdater : (store : Store) (IS : InboxShape) → Set₁ +InboxUpdater store IS = ValidMessageList store IS → ValidMessageList store IS + +record UpdatedInbox (store : Store) {store' : Store} (original : Inboxes store') (name : Name) : Set₂ where field updated-inboxes : Inboxes store' inboxes-valid : InboxesValid store updated-inboxes + others-unaffected : ∀ {name' IS' inb} → ¬ name ≡ name' → {p' : name' ↦ IS' ∈e store'} → InboxForPointer inb store' original p' → InboxForPointer inb store' updated-inboxes p' + open ValidMessageList -open UpdatedInboxes +open UpdatedInbox open NameSupply -- Update one of the inboxes in a list of inboxes. @@ -150,18 +216,29 @@ open NameSupply -- and a proof that all the messages are valid for the store. -- The update function returns a new list of the same type, -- and has to provide a proof that this list is also valid for the store -update-inboxes : {name : Name} → {IS : InboxShape} → +update-inbox : {name : Name} → {IS : InboxShape} → (store : Store) → - {store' : Store} → (inboxes : Inboxes store') → + {store' : Store} → + (inboxes : Inboxes store') → (InboxesValid store inboxes) → (name ↦ IS ∈e store') → - (f : ValidMessageList store IS → ValidMessageList store IS) → - UpdatedInboxes store inboxes -update-inboxes _ _ [] () _ -update-inboxes store (x ∷ inboxes) (px ∷ proofs) zero f with (f (record { inbox = x ; valid = px })) -... | updated = record { updated-inboxes = (inbox updated) ∷ inboxes ; inboxes-valid = (valid updated) ∷ proofs } -update-inboxes store (x ∷ inboxes) (px ∷ proofs) (suc p) f with (update-inboxes store inboxes proofs p f) -... | updated = record { updated-inboxes = x ∷ updated-inboxes updated ; inboxes-valid = px ∷ (inboxes-valid updated) } + (f : InboxUpdater store IS) → + UpdatedInbox store inboxes name +update-inbox _ _ [] () _ +update-inbox {name} store {store'} (x ∷ inboxes) (px ∷ proofs) zero f = + record { updated-inboxes = inbox updated ∷ inboxes ; inboxes-valid = (valid updated) ∷ proofs ; others-unaffected = unaffected } + where + updated = (f (record { inbox = x ; valid = px })) + unaffected : ∀ {name' IS' inb} → ¬ name ≡ name' → {p' : name' ↦ IS' ∈e store'} → InboxForPointer inb store' (x ∷ inboxes) p' → InboxForPointer inb store' (inbox updated ∷ inboxes) p' + unaffected pr zero = ⊥-elim (pr refl) + unaffected pr (suc ifp) = suc ifp +update-inbox {name} store {store'} (x ∷ inboxes) (px ∷ proofs) (suc p) f = + record { updated-inboxes = x ∷ updated-inboxes updated ; inboxes-valid = px ∷ inboxes-valid updated ; others-unaffected = unaffected } + where + updated = (update-inbox store inboxes proofs p f) + unaffected : ∀ {name' IS' inb} → ¬ name ≡ name' → {p' : name' ↦ IS' ∈e store'} → InboxForPointer inb store' (x ∷ inboxes) p' → InboxForPointer inb store' (x ∷ updated-inboxes updated) p' + unaffected pr zero = zero + unaffected pr (suc ifp) = suc (others-unaffected updated pr ifp) -- Move the actor that is at the top of the list, to the back of the list -- This is done to create a round-robin system for the actors, since run-env always picks the actor at the top @@ -179,34 +256,26 @@ top-actor-to-back env | x ∷ acts | (y ∷ prfs) = record ; blocked-valid = blocked-valid env ; messages-valid = messages-valid env ; name-supply = name-supply env + ; blocked-no-progress = blocked-no-progress env } --- Drop the actor that is at the top of the list completely. --- This is used when handling some monadic operations, when there is no following bind. --- The dropped actor is not put in the blocked list. -drop-top-actor : Env → Env -drop-top-actor env with (acts env) | (actors-valid env) -drop-top-actor env | [] | prfs = env -drop-top-actor env | _ ∷ rest | _ ∷ prfs = record - { acts = rest - ; blocked = blocked env - ; env-inboxes = env-inboxes env - ; store = store env - ; actors-valid = prfs - ; blocked-valid = blocked-valid env - ; messages-valid = messages-valid env - ; name-supply = name-supply env - } - -- An actor is still valid if we add a new inbox to the store, as long as that name is not used in the store before valid-actor-suc : ∀ {store actor IS} → (ns : NameSupply store) → ValidActor store actor → ValidActor (inbox# ns .name [ IS ] ∷ store) actor -valid-actor-suc ns va = record { - actor-has-inbox = suc {pr = ns .name-is-fresh (actor-has-inbox va)} (actor-has-inbox va) - ; references-have-pointer = ∀map (λ p → suc-p (ns .name-is-fresh (actual-has-pointer p)) p) (references-have-pointer va) - } - where - open ValidActor - open _comp↦_∈_ +valid-actor-suc ns va = + let open ValidActor + open _comp↦_∈_ + in record { + actor-has-inbox = suc {pr = ns .name-is-fresh (actor-has-inbox va)} (actor-has-inbox va) + ; references-have-pointer = ∀map (λ p → suc-p (ns .name-is-fresh (actual-has-pointer p)) p) (references-have-pointer va) + } + +valid-references-suc : ∀ {store references IS} → + (ns : NameSupply store) → + All (reference-has-pointer store) references → + All (reference-has-pointer (inbox# (ns .name) [ IS ] ∷ store)) references +valid-references-suc ns pointers = + let open _comp↦_∈_ + in ∀map (λ p → suc-p (ns .name-is-fresh (actual-has-pointer p)) p) pointers -- All the messages in an inbox are still valid if we add a new inbox to the store, as long as that name is not used in the store before messages-valid-suc : ∀ {store IS x} {inb : Inbox IS} → (ns : NameSupply store) → all-messages-valid store inb → all-messages-valid (inbox# ns .name [ x ] ∷ store) inb @@ -223,6 +292,11 @@ messages-valid-suc {store} {IS} {x} {nx ∷ _} ns (px ∷ vi) = message-valid-su message-valid-suc : (nx : NamedMessage IS) → message-valid store nx → message-valid (inbox# ns .name [ x ] ∷ store) nx message-valid-suc (NamedM x₁ x₂) px = fields-valid-suc px +is-blocked-suc : ∀ {store actor IS} {inbs : Inboxes store} {inb : Inbox IS} → (ns : NameSupply store) → IsBlocked store inbs actor → IsBlocked (inbox# ns .name [ IS ] ∷ store) (inb ∷ inbs) actor +is-blocked-suc ns (BlockedReturn at-return no-cont) = BlockedReturn at-return no-cont +is-blocked-suc ns (BlockedReceive at-receive p inbox-for-pointer) = BlockedReceive at-receive (suc {pr = ns .name-is-fresh p} p) (suc inbox-for-pointer) +is-blocked-suc ns (BlockedSelective at-selective p inb inbox-for-pointer filter-empty) = BlockedSelective at-selective (suc {pr = ns .name-is-fresh p} p) inb (suc inbox-for-pointer) filter-empty + -- Add a new actor to the environment. -- The actor is added to the top of the list of actors. add-top : ∀ {IS A post} → ActorState ∞ IS A [] post → Env → Env @@ -244,70 +318,109 @@ add-top {IS} {A} {post} m env = record ; blocked-valid = ∀map (valid-actor-suc (env .name-supply .supply)) (blocked-valid env) ; messages-valid = [] ∷ map-suc (store env) (messages-valid env) (env .name-supply .supply) ; name-supply = env .name-supply .next IS + ; blocked-no-progress = ∀map (is-blocked-suc (env .name-supply .supply)) (env .blocked-no-progress) } where + -- ad-hoc ∀map, because we are not using All here map-suc : (store : Store) → {store' : Store} → {inbs : Inboxes store'} → InboxesValid store inbs → (ns : NameSupply store) → InboxesValid (inbox# ns .name [ IS ] ∷ store) inbs map-suc store [] _ = [] map-suc store (x ∷ valid) ns = messages-valid-suc ns x ∷ (map-suc store valid ns) -record GetInbox (store : Store) (S : InboxShape) : Set₂ where + + +record GetInbox (store : Store) {store' : Store} (inboxes : Inboxes store') {name : Name} {S : InboxShape} (p : name ↦ S ∈e store') : Set₂ where field messages : Inbox S valid : all-messages-valid store messages + right-inbox : InboxForPointer messages store' inboxes p -- Get the messages of an inbox pointed to in the environment. -- This is just a simple lookup into the list of inboxes. -get-inbox : ∀ {name IS} → (env : Env) → name ↦ IS ∈e (store env) → GetInbox (store env) IS +get-inbox : ∀ {name IS} → (env : Env) → (p : name ↦ IS ∈e (store env)) → GetInbox (env .store) (env .env-inboxes) p get-inbox env point = loop (env-inboxes env) (messages-valid env) point where - loop : {store store' : Store} → (inbs : Inboxes store') → InboxesValid store inbs → ∀ {name IS} → name ↦ IS ∈e store' → GetInbox store IS + loop : {store store' : Store} → (inbs : Inboxes store') → InboxesValid store inbs → ∀ {name IS} → (p : name ↦ IS ∈e store') → GetInbox store inbs p loop _ [] () - loop (x ∷ _) (px ∷ _) zero = record { messages = x ; valid = px } - loop (_ ∷ inbs) (_ ∷ valid) (suc point) = loop inbs valid point + loop (x ∷ _) (px ∷ _) zero = record { messages = x ; valid = px ; right-inbox = zero } + loop (_ ∷ inbs) (_ ∷ inb-valid) (suc point) = + let rec = loop inbs inb-valid point + open GetInbox + in record { messages = rec .messages ; valid = rec .valid ; right-inbox = suc (rec .right-inbox) } + +open GetInbox + +record UnblockedActors {store store' : Store} {original : Inboxes store'} {n : Name} (updated : UpdatedInbox store original n) : Set₂ where + field + unblocked : List Actor + unblocked-updated : All (λ act → n ≡ name act) unblocked + unblocked-valid : All (ValidActor store) unblocked + still-blocked : List Actor + blocked-no-prog : All (IsBlocked store' (updated-inboxes updated)) still-blocked + blocked-valid : All (ValidActor store) still-blocked + +open UnblockedActors + +unblock-actors : + {store : Store} → + {original : Inboxes store} → + {n : Name} → + (updated : UpdatedInbox store original n) → + (blocked : List Actor) → + All (ValidActor store) blocked → + All (IsBlocked store original) blocked → + UnblockedActors updated +unblock-actors updated [] [] [] = record + { unblocked = [] + ; unblocked-updated = [] + ; unblocked-valid = [] + ; still-blocked = [] + ; blocked-no-prog = [] + ; blocked-valid = [] + } +unblock-actors {store} {original} {n} updated (x ∷ blckd) (v ∷ blckd-valid) (ib ∷ is-blocked) with (n ≟ (name x)) +... | yes p = + let rec = unblock-actors updated blckd blckd-valid is-blocked + in record + { unblocked = x ∷ rec .unblocked + ; unblocked-updated = p ∷ rec .unblocked-updated + ; unblocked-valid = v ∷ rec .unblocked-valid + ; still-blocked = rec .still-blocked + ; blocked-no-prog = rec .blocked-no-prog + ; blocked-valid = rec .blocked-valid + } +... | no ¬p = + let rec = unblock-actors updated blckd blckd-valid is-blocked + in record + { unblocked = rec .unblocked + ; unblocked-updated = rec .unblocked-updated + ; unblocked-valid = rec .unblocked-valid + ; still-blocked = x ∷ rec .still-blocked + ; blocked-no-prog = blocked-unaffected ib ∷ rec .blocked-no-prog + ; blocked-valid = v ∷ rec .blocked-valid + } + where + blocked-unaffected : IsBlocked store original x → IsBlocked store (updated-inboxes updated) x + blocked-unaffected (BlockedReturn x y) = BlockedReturn x y + blocked-unaffected (BlockedReceive x p y) = BlockedReceive x p (others-unaffected updated ¬p y) + blocked-unaffected (BlockedSelective x p a b c) = BlockedSelective x p a (others-unaffected updated ¬p b) c --- Updates an inbox in the environment --- Just a wrapper arround 'updateInboxes' update-inbox-env : ∀ {name IS} → (env : Env) → name ↦ IS ∈e (store env) → (f : ValidMessageList (store env) IS → ValidMessageList (store env) IS) → Env -update-inbox-env {name} {IS} env p f = record - { acts = acts env - ; blocked = blocked env - ; env-inboxes = updated-inboxes updated - ; store = store env - ; actors-valid = actors-valid env - ; blocked-valid = blocked-valid env - ; messages-valid = inboxes-valid updated - ; name-supply = env .name-supply - } - where - updated = update-inboxes (store env) (env-inboxes env) (messages-valid env) p f - --- Move an actor from the blocked list to the actors list. --- Simply looks through the names of all blocked actors and moves those (should be just 1 or 0) with the same name. --- IF an actor still doesn't have a way to progress (should never happen), --- it will just get added back to the blocked list the next time it is processed. -unblock-actor : Env → Name → Env -unblock-actor env name = newEnv (loop (blocked env) (blocked-valid env)) - where - loop : (blocked : List Actor) → (blockedValid : All (ValidActor (store env)) blocked) → - (Σ[ blockedAfter ∈ List Actor ] All (ValidActor (store env)) blockedAfter) × (Σ[ unblocked ∈ List Actor ] All (ValidActor (store env)) unblocked) - loop [] [] = ([] , []) , ([] , []) - loop (x ∷ blocked) (px ∷ blockedValid) with (loop blocked blockedValid) - ... | (blockedAfter , baValid) , unblocked , unblockedValid with (Actor.name x ≟ name) - ... | yes p = (blockedAfter , baValid) , ((x ∷ unblocked) , px ∷ unblockedValid) - ... | no ¬p = ((x ∷ blockedAfter) , (px ∷ baValid)) , unblocked , unblockedValid - newEnv : Σ (Σ (List Actor) (All (ValidActor (store env)))) - (λ _ → Σ (List Actor) (All (ValidActor (store env)))) → Env - newEnv ((ba , baValid) , unblocked , unblockedValid) = record - { acts = acts env ++ unblocked - ; blocked = ba - ; env-inboxes = env-inboxes env - ; store = store env - ; actors-valid = ++⁺ (actors-valid env) unblockedValid - ; blocked-valid = baValid - ; messages-valid = messages-valid env - ; name-supply = env .name-supply - } +update-inbox-env {name} {IS} env p f = + let + updated = update-inbox (store env) (env-inboxes env) (messages-valid env) p f + unblock-split = unblock-actors updated (blocked env) (blocked-valid env) (blocked-no-progress env) + in record { + acts = (unblocked unblock-split) ++ acts env + ; blocked = still-blocked unblock-split + ; env-inboxes = updated-inboxes updated + ; store = store env + ; actors-valid = ++⁺ (unblock-split .unblocked-valid) (env .actors-valid) + ; blocked-valid = unblock-split .blocked-valid + ; messages-valid = inboxes-valid updated + ; name-supply = env .name-supply + ; blocked-no-progress = unblock-split .blocked-no-prog + } record FoundReference (store : Store) (S : InboxShape) : Set₂ where field @@ -325,6 +438,8 @@ lookup-reference _ (_ ∷ refs) (_ ∷ prfs) refl (S px) = lookup-reference _ re lookup-reference-act : ∀ {store actor ToIS} → ValidActor store actor → ToIS ∈ (pre actor) → FoundReference store ToIS lookup-reference-act {store} {actor} {ToIS} va ref = lookup-reference (pre actor) (Actor.references actor) (ValidActor.references-have-pointer va) (pre-eq-refs actor) ref + + open _comp↦_∈_ open FoundReference @@ -343,25 +458,25 @@ record LiftedReferences (lss gss : TypingContext) (references : List NamedInbox) subset-inbox : lss ⊆ gss contained : List NamedInbox subset : contained ⊆ references - contained-eq-inboxes : lss ≡ map shape contained + contained-eq-inboxes : map shape contained ≡ lss open LiftedReferences -- Convert a subset for preconditions to a subset for references lift-references : ∀ {lss gss} → lss ⊆ gss → (references : List NamedInbox) → map shape references ≡ gss → LiftedReferences lss gss references -lift-references [] refs refl = record - { subset-inbox = [] - ; contained = [] - ; subset = [] - ; contained-eq-inboxes = refl - } +lift-references [] refs refl = record { + subset-inbox = [] + ; contained = [] + ; subset = [] + ; contained-eq-inboxes = refl + } lift-references (_∷_ {y} {xs} x₁ subs) refs refl with (lift-references subs refs refl) -... | q = record - { subset-inbox = x₁ ∷ subs - ; contained = (lookup-parallel x₁ refs shape refl) ∷ contained q - ; subset = (translate-∈ x₁ refs shape refl) ∷ (subset q) - ; contained-eq-inboxes = combine y (shape (lookup-parallel x₁ refs shape refl)) xs (map shape (contained q)) contained-el-ok (contained-eq-inboxes q) - } +... | q = record { + subset-inbox = x₁ ∷ subs + ; contained = contained-el ∷ contained q + ; subset = (translate-∈ x₁ refs shape refl) ∷ (subset q) + ; contained-eq-inboxes = combine contained-el-shape y (map shape (contained q)) xs (sym contained-el-ok) (contained-eq-inboxes q) + } where contained-el : NamedInbox contained-el = lookup-parallel x₁ refs shape refl @@ -371,32 +486,88 @@ lift-references (_∷_ {y} {xs} x₁ subs) refs refl with (lift-references subs combine : (a b : InboxShape) → (as bs : TypingContext) → (a ≡ b) → (as ≡ bs) → (a ∷ as ≡ b ∷ bs) combine a .a as .as refl refl = refl +data LiftActor : Actor → Actor → Set₂ where + CanBeLifted : + ∀ {A A' post post'} + {IS name references} + {lss gss} + {per} + {computation computation'} → + (lr : LiftedReferences lss gss references) → + LiftActor + (record + { inbox-shape = IS + ; A = A + ; references = references + ; pre = gss + ; pre-eq-refs = per + ; post = post + ; computation = computation + ; name = name + }) + (record + { inbox-shape = IS + ; A = A' + ; references = lr .contained + ; pre = lss + ; pre-eq-refs = lr .contained-eq-inboxes + ; post = post' + ; computation = computation' + ; name = name + }) + +lift-valid-actor : ∀ {store} {act act' : Actor} → + LiftActor act act' → + ValidActor store act → + ValidActor store act' +lift-valid-actor (CanBeLifted lr) va = + record { + actor-has-inbox = va .actor-has-inbox + ; references-have-pointer = All-⊆ (lr .subset) (va .references-have-pointer) + } + + + -- We can replace the actors in an environment if they all are valid for the current store. replace-actors : (env : Env) → (actors : List Actor) → All (ValidActor (store env)) actors → Env replace-actors env actors actorsValid = record { acts = actors - ; blocked = blocked env - ; env-inboxes = env-inboxes env - ; store = store env + ; blocked = env .blocked + ; env-inboxes = env .env-inboxes + ; store = env .store ; actors-valid = actorsValid - ; blocked-valid = blocked-valid env - ; messages-valid = messages-valid env + ; blocked-valid = env .blocked-valid + ; messages-valid = env .messages-valid ; name-supply = env .name-supply + ; blocked-no-progress = env .blocked-no-progress } --- We can replace both the running and blocked actors in an environment if they all are valid for the current store. -replace-actors+blocked : (env : Env) → - (actors : List Actor) → All (ValidActor (store env)) actors → - (blocked : List Actor) → All (ValidActor (store env)) blocked → Env -replace-actors+blocked env actors actorsValid blocked blockedValid = record { - acts = actors +replace-focused : {act : Actor} → (env : Env) → Focus act env → + (act' : Actor) → + (valid' : ValidActor (env .store) act') → + Env +replace-focused env@record { + acts = _ ∷ rest + ; actors-valid = _ ∷ rest-valid + } Focused act' valid' = + replace-actors env (act' ∷ rest) (valid' ∷ rest-valid) + +block-focused : {act : Actor} → (env : Env) → Focus act env → IsBlocked (env .store) (env .env-inboxes) act → Env +block-focused env@record { + acts = actor ∷ rest ; blocked = blocked - ; env-inboxes = env-inboxes env - ; store = store env - ; actors-valid = actorsValid - ; blocked-valid = blockedValid - ; messages-valid = messages-valid env + ; actors-valid = actor-valid ∷ rest-valid + ; blocked-valid = blocked-valid + } Focused blckd = record { + acts = rest + ; blocked = actor ∷ blocked + ; store = env .store + ; env-inboxes = env .env-inboxes ; name-supply = env .name-supply + ; actors-valid = rest-valid + ; blocked-valid = actor-valid ∷ blocked-valid + ; messages-valid = env .messages-valid + ; blocked-no-progress = blckd ∷ env .blocked-no-progress } -- Takes a named message and a proof that the named message is valid for the store. @@ -428,14 +599,6 @@ unname-field : ∀ {x} → named-field-content x → receive-field-content x unname-field {ValueType x₁} nfc = nfc unname-field {ReferenceType x₁} nfc = _ -unname-message : ∀ {S} → NamedMessage S → Message S -unname-message (NamedM x fields) = Msg x (do-the-work fields) - where - do-the-work : ∀ {MT} → All named-field-content MT → All receive-field-content MT - do-the-work {[]} nfc = [] - do-the-work {ValueType x₁ ∷ MT} (px ∷ nfc) = px ∷ (do-the-work nfc) - do-the-work {ReferenceType x₁ ∷ MT} (px ∷ nfc) = _ ∷ do-the-work nfc - extract-inboxes : ∀ {MT} → All named-field-content MT → List NamedInbox extract-inboxes [] = [] extract-inboxes (_∷_ {ValueType _} _ ps) = extract-inboxes ps @@ -453,15 +616,16 @@ reference-names (_∷_ {ReferenceType x} name ps) = name ∷ reference-names ps ++-diff [] .[] c refl = refl ++-diff (x ∷ a) .(x ∷ a) c refl = refl +add-fields++ : ∀ MT → (x₁ : All named-field-content MT) → map shape (extract-inboxes x₁) ≡ extract-references MT +add-fields++ [] [] = refl +add-fields++ (ValueType x ∷ MT) (px ∷ x₁) = add-fields++ MT x₁ +add-fields++ (ReferenceType x ∷ MT) (px ∷ x₁) = cong (_∷_ x) (add-fields++ MT x₁) + add-references++ : ∀ {S store} → (nm : NamedMessage S) → message-valid store nm → ∀ w → map shape (named-inboxes nm) ++ w ≡ add-references w (unname-message nm) add-references++ msg@(NamedM {MT} x x₁) p w = halp (add-fields++ MT x₁) where halp : map shape (extract-inboxes x₁) ≡ extract-references MT → map shape (extract-inboxes x₁) ++ w ≡ extract-references MT ++ w halp p = ++-diff (map shape (extract-inboxes x₁)) (extract-references MT) w p - add-fields++ : ∀ MT → (x₁ : All named-field-content MT) → map shape (extract-inboxes x₁) ≡ extract-references MT - add-fields++ [] [] = refl - add-fields++ (ValueType x ∷ MT) (px ∷ x₁) = add-fields++ MT x₁ - add-fields++ (ReferenceType x ∷ MT) (px ∷ x₁) = cong (_∷_ x) (add-fields++ MT x₁) valid++ : ∀ {S store} → (nm : NamedMessage S) → message-valid store nm → ∀ {w} → All (reference-has-pointer store) w → @@ -483,9 +647,10 @@ compatible-handles : ∀ store x refs (px : (map shape refs) ⊢>: x) (w : FoundReference store (actual px)) → x ⊆ actual (reference w) -compatible-handles store x refs px w with (actual-handles-requested px) -... | a with (actual-handles-wanted (reference w)) -... | b = ⊆-trans a b +compatible-handles store x refs px w = + let a = actual-handles-requested px + b = actual-handles-wanted (reference w) + in ⊆-trans a b make-pointer-compatible : ∀ store x refs (px : (map shape refs) ⊢>: x) → @@ -502,47 +667,17 @@ make-pointers-compatible : ∀ {MT} store pre refs (eq : map shape refs ≡ pre) FieldsHavePointer store (name-fields pre refs rhp fields eq) make-pointers-compatible store pre refs eq [] rhp = [] make-pointers-compatible store _ refs refl (_∷_ {ValueType x} px fields) rhp = FhpV ∷ make-pointers-compatible store _ refs refl fields rhp -make-pointers-compatible store _ refs refl (_∷_ {ReferenceType x} px fields) rhp = FhpR (make-pointer-compatible store x refs px rhp foundFw) ∷ (make-pointers-compatible store _ refs refl fields rhp) - where - foundFw : FoundReference store (actual px) - foundFw = lookup-reference _ refs rhp refl (actual-is-sendable px) - -record SplitList {a : Level} {A : Set a} (ls : List A) : Set (lsuc a) where - field - heads : List A - el : A - tails : List A - is-ls : (heads) ++ (el ∷ tails) ≡ ls - -data FoundInList {a : Level} {A : Set a} (ls : List A) (f : A → Bool) : Set (lsuc a) where - Found : (split : SplitList ls) → (f (SplitList.el split) ≡ true) → FoundInList ls f - Nothing : FoundInList ls f - -find-split : {a : Level} {A : Set a} (ls : List A) (f : A → Bool) → FoundInList ls f -find-split [] f = Nothing -find-split (x ∷ ls) f with (f x) | (inspect f x) -... | false | p = add-x (find-split ls f) - where - add-x : FoundInList ls f → FoundInList (x ∷ ls) f - add-x (Found split x₁) = Found (record { heads = x ∷ heads split ; el = el split ; tails = tails split ; is-ls = cong (_∷_ x) (is-ls split) }) x₁ - where open SplitList - add-x Nothing = Nothing -... | true | [ eq ] = Found (record { heads = [] ; el = x ; tails = ls ; is-ls = refl }) eq +make-pointers-compatible store _ refs refl (_∷_ {ReferenceType x} px fields) rhp = + let foundFw = lookup-reference _ refs rhp refl (actual-is-sendable px) + in FhpR (make-pointer-compatible store x refs px rhp foundFw) ∷ (make-pointers-compatible store _ refs refl fields rhp) -- Removes the next message from an inbox. -- This is a no-op if there are no messages in the inbox. remove-found-message : {S : InboxShape} → {store : Store} → (filter : MessageFilter S) → (ValidMessageList store S → ValidMessageList store S) remove-found-message f record { inbox = [] ; valid = [] } = record { inbox = [] ; valid = [] } remove-found-message {s} {store} f record { inbox = (x ∷ inbox₁) ; valid = vx ∷ valid₁ } with (f (unname-message x)) -... | false = add-x (remove-found-message f (record { inbox = inbox₁ ; valid = valid₁ })) - where - add-x : ValidMessageList store s → ValidMessageList store s - add-x record { inbox = inbox ; valid = valid } = record { inbox = x ∷ inbox ; valid = vx ∷ valid } +... | false = + let vml = remove-found-message f (record { inbox = inbox₁ ; valid = valid₁ }) + open ValidMessageList + in record { inbox = x ∷ vml .inbox ; valid = vx ∷ vml .valid } ... | true = record { inbox = inbox₁ ; valid = valid₁ } - -split-all-el : ∀ {a p} {A : Set a} {P : A → Set p} (ls : List A) → All P ls → (sl : SplitList ls) → (P (SplitList.el sl)) -split-all-el [] ps record { heads = [] ; el = el ; tails = tails ; is-ls = () } -split-all-el [] ps record { heads = (x ∷ heads) ; el = el ; tails = tails ; is-ls = () } -split-all-el (x ∷ ls) (px ∷ ps) record { heads = [] ; el = .x ; tails = .ls ; is-ls = refl } = px -split-all-el (x ∷ ls) (px ∷ ps) record { heads = (x₁ ∷ heads) ; el = el ; tails = tails ; is-ls = refl } = - split-all-el ls ps (record { heads = heads ; el = el ; tails = tails ; is-ls = refl }) diff --git a/src/Selective/Examples/ActiveObjects.agda b/src/Selective/Examples/ActiveObjects.agda new file mode 100644 index 0000000..5c0d84c --- /dev/null +++ b/src/Selective/Examples/ActiveObjects.agda @@ -0,0 +1,177 @@ +module Selective.Examples.ActiveObjects where + +open import Selective.ActorMonad public +open import Selective.Examples.Channel public +open import Selective.Examples.Call2 public +open import Membership using ( + _∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] + ; ⊆-refl ; ⊆-trans ; ⊆-suc ; translate-⊆ + ; lookup-all ; ⊆++-l-refl + ) +open import Data.List using (List ; _∷_ ; [] ; _++_ ; map) +open import Data.List.All using (All ; _∷_ ; []) renaming (map to ∀map) +open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; _≟_ ) +open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) +open import Level using (Lift ; lift) renaming (zero to lzero ; suc to lsuc) +open import Size + +open ChannelType +open ChannelInitiation + + +active-request-type : ChannelInitiation → InboxShape +active-request-type record { request = .[] ; response = response ; request-tagged = [] } = [] +active-request-type record { request = .(_ ∷ _) ; response = response ; request-tagged = (px ∷ pxs) } = + let rec = active-request-type (record { request = _ ; response = response ; request-tagged = pxs }) + in extra-fields-shape px ∷ rec + +state-vars : ∀ {ci} {st : Set₁} → (st → TypingContext) → Message ci → InboxShape → st → TypingContext +state-vars f input caller state = caller ∷ add-references (f state) input + + +active-reply-needed-fields : ∀ mt → IsChannelMessage mt → MessageType +active-reply-needed-fields _ (HasTag MT) = MT + +active-reply-type : ChannelType → InboxShape +active-reply-type record { channel-shape = [] } = [] +active-reply-type record { channel-shape = (x ∷ xs) ; all-tagged = (px ∷ pxs) } = + let rec = active-reply-type (record { channel-shape = xs ; all-tagged = pxs }) + in active-reply-needed-fields x px ∷ rec + +record ActiveReply (ci : ChannelInitiation) (state-type : Set₁) (var-f : state-type → TypingContext) (input : Message (active-request-type ci)) (caller : InboxShape) : Set₁ where + field + new-state : state-type + reply : SendMessage (active-reply-type (ci .response)) (state-vars var-f input caller new-state) + +reply-vars : ∀ {st ci var-f input} → (st → TypingContext) → Message (active-request-type ci) → (caller : InboxShape) → ActiveReply ci st var-f input caller → TypingContext +reply-vars f input caller ar = state-vars f input caller (ActiveReply.new-state ar) + +active-method : InboxShape → (state-type : Set₁) → (state-type → TypingContext) → ChannelInitiation → Set₂ +active-method IS st var-f ci = + let input-type = Message (active-request-type ci) + in {i : Size} → + {caller : InboxShape} → + (input : input-type) → + (state : st) → + ∞ActorM i IS + (ActiveReply ci st var-f input caller) + (caller ∷ add-references (var-f state) input) + (reply-vars var-f input caller) + +active-inbox-shape : List ChannelInitiation → InboxShape +active-inbox-shape [] = [] +active-inbox-shape (x ∷ lci) = + let rec = active-inbox-shape lci + in x .request ++ rec + +record ActiveObject : Set₂ where + field + state-type : Set₁ + vars : state-type → TypingContext + methods : List ChannelInitiation + handlers : All (active-method (active-inbox-shape methods) state-type vars) methods + +open ActiveObject + +active-caller : (methods : List ChannelInitiation) → + Message (active-inbox-shape methods) → + InboxShape +active-caller methods (Msg x f) = active-caller' methods x + where + active-caller' : {MT : MessageType} → + (methods : List ChannelInitiation) → + MT ∈ active-inbox-shape methods → + InboxShape + active-caller' [] () + active-caller' (record { request = [] } ∷ methods) p = active-caller' methods p + active-caller' (record { request = x ∷ _ ; response = response } ∷ _) Z = response .channel-shape + active-caller' (record { request = _ ∷ xs ; response = response ; request-tagged = _ ∷ pxs } ∷ methods) (S p) = + active-caller' (record { request = xs ; response = response ; request-tagged = pxs } ∷ methods) p + +forget-message : ∀ {i Γ} → + {IS IS' : InboxShape} → + (m : Message IS) → + ∞ActorM i IS' ⊤₁ (add-references Γ m) (λ _ → Γ) +forget-message (Msg x x₁) = strengthen (⊆++-l-refl _ _) + +data InEither {a} {A : Set a} (v : A) (xs ys : List A) : Set a where + Left : (v ∈ xs) → InEither v xs ys + Right : (v ∈ ys) → InEither v xs ys + +∈++ : ∀ {a} {A : Set a} {v : A} → (xs ys : List A) → (v ∈ (xs ++ ys)) → InEither v xs ys +∈++ [] ys p = Right p +∈++ (x ∷ xs) ys Z = Left Z +∈++ (x ∷ xs) ys (S p) with (∈++ xs ys p) +... | Left q = Left (S q) +... | Right q = Right q + +invoke-active-method : {i : Size} → + (ac : ActiveObject) → + (input : Message (active-inbox-shape (ac .methods))) → + (state : ac .state-type) → + ∞ActorM i (active-inbox-shape (ac .methods)) + (ac .state-type) (add-references (ac .vars state) input) (λ x → add-references (ac .vars x) input) +invoke-active-method ac (Msg x f) state = invoke f (ac .methods) (ac .handlers) x + where + translate-invoke-pointer : {ci : ChannelInitiation} → + {MT : MessageType} → + (ValueType UniqueTag ∷ ReferenceType (ci .response .channel-shape) ∷ MT) ∈ ci .request → + MT ∈ active-request-type ci + translate-invoke-pointer {record { request-tagged = HasTag+Ref MT ∷ _ }} Z = Z + translate-invoke-pointer {record { response = response ; request-tagged = _ ∷ rt }} (S p) = + let rec = translate-invoke-pointer {record { request = _ ; response = response ; request-tagged = rt }} p + in S rec + translate-send-pointer : ∀ {ct MT} → + MT ∈ active-reply-type ct → + (TagField ∷ MT) ∈ ct .channel-shape + translate-send-pointer {record { channel-shape = [] }} () + translate-send-pointer {record { all-tagged = HasTag MT ∷ _ }} Z = Z + translate-send-pointer {record { channel-shape = x ∷ xs ; all-tagged = px ∷ pxs }} (S p) = S (translate-send-pointer p) + invoke' : {i : Size} {MT : MessageType} → + All receive-field-content MT → + (ci : ChannelInitiation) → + active-method (active-inbox-shape (ac .methods)) (ac .state-type) (ac .vars) ci → + MT ∈ (ci .request) → + IsRequestMessage (ci .response .channel-shape) MT → + ∞ActorM i (active-inbox-shape (ac .methods)) (ac .state-type) (extract-references MT ++ ac .vars state) (λ st → extract-references MT ++ ac .vars st) + invoke' (tag ∷ _ ∷ f) ci handler p (HasTag+Ref MT) = + let + active-message : Message (active-request-type ci) + active-message = Msg (translate-invoke-pointer p) f + in do + record { new-state = new-state ; reply = SendM which fields } ← handler active-message state + send Z (SendM (translate-send-pointer which) (lift tag ∷ fields)) + return₁ new-state + invoke : {i : Size} {MT : MessageType} → + All receive-field-content MT → + (cis : List ChannelInitiation) → + All (active-method (active-inbox-shape (ac .methods)) (ac .state-type) (ac .vars)) cis → + MT ∈ active-inbox-shape cis → + ∞ActorM i (active-inbox-shape (ac .methods)) (ac .state-type) (add-references-static (ac .vars state) MT) (λ st → add-references-static (ac .vars st) MT) + invoke _ _ [] () + invoke f (ci ∷ _) (_ ∷ _) x with (∈++ (ci .request) _ x) + invoke f (ci ∷ _) (handler ∷ _) x | Left q = + let irm = lookup-all q (ci .request-tagged) + in invoke' f ci handler q irm + invoke f (_ ∷ cis) (_ ∷ handlers) x | Right q = invoke f cis handlers q + +handle-active-method : {i : Size} → + (ac : ActiveObject) → + (input : Message (active-inbox-shape (ac .methods))) → + (state : ac .state-type) → + ∞ActorM i (active-inbox-shape (ac .methods)) + (ac .state-type) (add-references (ac .vars state) input) (ac .vars) +handle-active-method ac input state = + do + state' ← (invoke-active-method ac input state) + forget-message input + return₁ state' + +run-active-object : {i : Size} → + (ac : ActiveObject) → + (state : ac .state-type) → + ∞ActorM i (active-inbox-shape (ac .methods)) (ac .state-type) ((ac .vars) state) (ac .vars) +run-active-object ac state .force = + receive ∞>>= λ m → + handle-active-method ac m state >>= λ state' → + run-active-object ac state' diff --git a/src/Selective/Examples/Bookstore.agda b/src/Selective/Examples/Bookstore.agda new file mode 100644 index 0000000..6c7b49c --- /dev/null +++ b/src/Selective/Examples/Bookstore.agda @@ -0,0 +1,346 @@ +module Selective.Examples.Bookstore where + +open import Selective.ActorMonad public +open import Selective.Examples.Call using (UniqueTag ; call) +open import Data.List using (List ; _∷_ ; [] ; map ; _++_ ; reverse ; _∷ʳ_ ; length) +open import Data.List.All using (All ; _∷_ ; []) +open import Data.Bool using (Bool ; false ; true) +open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; _≟_ ; pred ; ⌈_/2⌉ ; _≤?_ ; _∸_ ; _≤_ ; z≤n ; s≤s ; _<_ ; _≰_ ) +open import Data.Nat.Properties using (≤-antisym ; ≰⇒>) +open import Data.Maybe as Maybe using (Maybe ; just ; nothing) +open import Data.String using (String ; primStringEquality) renaming (_++_ to _||_) +open import Size +open import Level using (Lift ; lift) renaming (zero to lzero ; suc to lsuc) +open import Data.List.Any using (here ; there) +open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong) +open import Relation.Nullary using (yes ; no) +open import Relation.Nullary.Decidable using (⌊_⌋) +open import Membership using (_∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] ; ⊆-refl ; ⊆-suc ; ⊆++-refl ; translate-⊆) +open import Data.Unit using (⊤ ; tt) + +open import Data.List.Properties + +open import Category.Monad + +open import Debug +open import Data.Nat.Show using (show) + +BookTitle = String +Money = ℕ + +data BuyerRole : Set where + Buyer1 Buyer2 : BuyerRole + +record Book : Set where + field + title : BookTitle + price : Money + +-- =========== +-- GET QUOTE +-- =========== + +GetQuoteReply : MessageType +GetQuoteReply = ValueType UniqueTag ∷ ValueType (Maybe Book) ∷ [] + +GetQuoteReplyInterface : InboxShape +GetQuoteReplyInterface = GetQuoteReply ∷ [] + +GetQuote : MessageType +GetQuote = ValueType UniqueTag ∷ ReferenceType GetQuoteReplyInterface ∷ ValueType BookTitle ∷ [] + +-- ====================== +-- PROPOSE CONTRIBUTION +-- ====================== + +record Contribution : Set where + field + book : Book + money : Money + +ContributionMessage : MessageType +ContributionMessage = ValueType Contribution ∷ [] + +-- =============== +-- AGREE OR QUIT +-- =============== + +data AgreeChoice : Set where + AGREE QUIT : AgreeChoice + +AgreeDecision : MessageType +AgreeDecision = ValueType AgreeChoice ∷ [] + +-- ================ +-- TRANSFER MONEY +-- ================ + +Transfer : MessageType +Transfer = ValueType BuyerRole ∷ ValueType Contribution ∷ [] + +-- ============ +-- INTERFACES +-- ============ + +Buyer1-to-Seller : InboxShape +Buyer1-to-Seller = GetQuote ∷ Transfer ∷ [] + +Buyer2-to-Seller : InboxShape +Buyer2-to-Seller = AgreeDecision ∷ Transfer ∷ [] + +Buyer1-to-Buyer2 : InboxShape +Buyer1-to-Buyer2 = ContributionMessage ∷ [] + +Buyer2-to-Buyer1 : InboxShape +Buyer2-to-Buyer1 = AgreeDecision ∷ [] + +SellerInterface : InboxShape +SellerInterface = GetQuote ∷ AgreeDecision ∷ Transfer ∷ [] + +Buyer1Interface : InboxShape +Buyer1Interface = (ReferenceType Buyer1-to-Seller ∷ []) ∷ (ReferenceType Buyer1-to-Buyer2 ∷ []) ∷ GetQuoteReply ∷ AgreeDecision ∷ [] + +Buyer2Interface : InboxShape +Buyer2Interface = (ReferenceType Buyer2-to-Seller ∷ []) ∷ (ReferenceType Buyer2-to-Buyer1 ∷ []) ∷ ContributionMessage ∷ [] + +-- ======== +-- COMMON +-- ======== + +book1 : BookTitle +book1 = "Crime and Punishment" + +transfer-money : ∀ {i IS Seller Γ} → + Γ ⊢ Seller → + (Transfer ∷ []) <: Seller → + BuyerRole → + Book → + Money → + ∞ActorM i IS ⊤₁ Γ (λ _ → Γ) +transfer-money p sub role book money = p ![t: translate-⊆ sub Z ] ((lift role) ∷ (lift (record { book = book ; money = money })) ∷ []) +-- ======== +-- SELLER +-- ======== + +same-buyer-role : BuyerRole → BuyerRole → Bool +same-buyer-role Buyer1 Buyer1 = true +same-buyer-role Buyer1 Buyer2 = false +same-buyer-role Buyer2 Buyer1 = false +same-buyer-role Buyer2 Buyer2 = true + +data TransactionStatus (book : Book) (c1 c2 : Contribution) : Set where + TooLittleMoney : (Contribution.money c1 + Contribution.money c2) < (Book.price book) → TransactionStatus book c1 c2 + Accepted : (Contribution.money c1 + Contribution.money c2) ≡ (Book.price book) → TransactionStatus book c1 c2 + TooMuchMoney : (Book.price book) < (Contribution.money c1 + Contribution.money c2) → TransactionStatus book c1 c2 + +transaction-status? : ∀ book c1 c2 → TransactionStatus book c1 c2 +transaction-status? book c1 c2 with (Contribution.money c1 + Contribution.money c2 ≤? Book.price book) | (Book.price book ≤? Contribution.money c1 + Contribution.money c2) +transaction-status? book c1 c2 | yes p | yes q = Accepted (≤-antisym p q) +transaction-status? book c1 c2 | yes p | no ¬p = TooLittleMoney (≰⇒> ¬p) +transaction-status? book c1 c2 | no ¬p | q = TooMuchMoney (≰⇒> ¬p) + +seller : ∀ {i} → ActorM i SellerInterface ⊤₁ [] (λ _ → []) +seller = begin do + record {msg = Msg Z (tag ∷ _ ∷ title ∷ []) } ← selective-receive select-quote + where + record { msg = (Msg (S _) _) ; msg-ok = () } + let maybe-book = find-book known-books title + (Z ![t: Z ] (lift tag ∷ (lift maybe-book ∷ []))) + after-book-quote maybe-book + where + select-quote : MessageFilter SellerInterface + select-quote (Msg Z _) = true + select-quote _ = false + known-books : List Book + known-books = record { title = book1 ; price = 37 } ∷ [] + find-book : List Book → BookTitle → Maybe Book + find-book [] title = nothing + find-book (book ∷ books) title with (primStringEquality (Book.title book) title) + ... | true = just book + ... | false = find-book books title + select-decision : MessageFilter SellerInterface + select-decision (Msg (S Z) _) = true + select-decision _ = false + wait-for-decision : ∀ {i Γ} → + ∞ActorM i SellerInterface (Lift AgreeChoice) Γ (λ _ → Γ) + wait-for-decision = do + record { msg = Msg (S Z) (ac ∷ []) } ← (selective-receive select-decision) + where + record { msg = (Msg Z _) ; msg-ok = () } + record { msg = (Msg (S (S _)) _) ; msg-ok = () } + return ac + select-contribution-from : BuyerRole → MessageFilter SellerInterface + select-contribution-from br (Msg (S (S Z)) (br' ∷ _)) = same-buyer-role br br' + select-contribution-from _ _ = false + wait-for-money-from : ∀ {i Γ} → + BuyerRole → + ∞ActorM i SellerInterface (Lift Contribution) Γ (λ _ → Γ) + wait-for-money-from br = do + record { msg = Msg (S (S Z)) (_ ∷ contribution ∷ []) } ← (selective-receive (select-contribution-from br)) + where + record { msg = (Msg Z _) ; msg-ok = () } + record { msg = (Msg (S Z) _) ; msg-ok = () } + record { msg = (Msg (S (S (S _))) _) ; msg-ok = () } + return contribution + transaction-message : Book → Contribution → Contribution → String + transaction-message book c1 c2 with (transaction-status? book c1 c2) + ... | Accepted _ = "Accepted purchase of " || Book.title book || " for $" || show (Book.price book) + ... | TooLittleMoney p = "Received too little money for " || Book.title book || ". $" || show (Book.price book) || " - $" || show (Contribution.money c1) || " - $" || show (Contribution.money c2) || " = $" || show (Book.price book ∸ Contribution.money c1 ∸ Contribution.money c2) + ... | TooMuchMoney p = "Received too much money for " || Book.title book || ". $" || show (Book.price book) || " - $" || show (Contribution.money c1) || " - $" || show (Contribution.money c2) || " = -$" || show ((Contribution.money c1 + Contribution.money c2) ∸ Book.price book) + after-book-quote : ∀ {i} → + Maybe Book → + ∞ActorM i SellerInterface ⊤₁ (GetQuoteReplyInterface ∷ []) (λ _ → []) + after-book-quote (just book) = do + lift AGREE ← wait-for-decision + where + lift QUIT → debug "seller sees that transaction was quit" (strengthen []) + lift contrib1 ← wait-for-money-from Buyer1 + lift contrib2 ← wait-for-money-from Buyer2 + debug (transaction-message book contrib1 contrib2) (strengthen []) + after-book-quote nothing = strengthen [] + +-- ========= +-- BUYER 1 +-- ========= + +buyer1 : ∀ {i} → ActorM i Buyer1Interface ⊤₁ [] (λ _ → []) +buyer1 = begin do + wait-for-seller + lift (just book) ← get-quote Z 0 book1 + where + (lift nothing) → strengthen [] + wait-for-buyer2 + let my-contribution = ⌈ Book.price book /2⌉ + send-contribution Z book my-contribution + lift AGREE ← wait-for-decision + where + lift QUIT → debug "buyer1 sees that transaction was quit" (strengthen []) + (transfer-money (S Z) (⊆-suc ⊆-refl) Buyer1 book my-contribution) + (strengthen []) + where + select-seller : MessageFilter Buyer1Interface + select-seller (Msg Z _) = true + select-seller (Msg (S _) _) = false + wait-for-seller : ∀ {i Γ} → ∞ActorM i Buyer1Interface ⊤₁ Γ (λ _ → Buyer1-to-Seller ∷ Γ) + wait-for-seller = do + record { msg = Msg Z _ } ← (selective-receive select-seller) + where + record { msg = (Msg (S _) _) ; msg-ok = () } + return _ + select-buyer2 : MessageFilter Buyer1Interface + select-buyer2 (Msg (S Z) _) = true + select-buyer2 _ = false + wait-for-buyer2 : ∀ {i Γ} → ∞ActorM i Buyer1Interface ⊤₁ Γ (λ _ → Buyer1-to-Buyer2 ∷ Γ) + wait-for-buyer2 = do + record {msg = Msg (S Z) _ } ← selective-receive select-buyer2 + where + record { msg = (Msg Z _) ; msg-ok = () } + record { msg = (Msg (S (S _)) _) ; msg-ok = () } + return _ + get-quote : ∀ {i Γ} → + Γ ⊢ Buyer1-to-Seller → + UniqueTag → + BookTitle → + ∞ActorM i Buyer1Interface (Lift (Maybe Book)) Γ (λ _ → Γ) + get-quote p tag title = do + record { msg = Msg (S (S Z)) (_ ∷ book ∷ []) ; msg-ok = msg-ok } ← (call p Z tag ((lift title) ∷ []) ((S (S Z)) ∷ []) Z) + where + record { msg = (Msg Z (_ ∷ _)) ; msg-ok = () } + record { msg = (Msg (S Z) (_ ∷ _)) ; msg-ok = () } + record { msg = (Msg (S (S (S Z))) _) ; msg-ok = () } + record { msg = (Msg (S (S (S (S _)))) _) ; msg-ok = () } + return book + send-contribution : ∀ {i Γ} → + Γ ⊢ Buyer1-to-Buyer2 → + Book → + Money → + ∞ActorM i Buyer1Interface ⊤₁ Γ (λ _ → Γ) + send-contribution p book money = p ![t: Z ] ((lift (record { book = book ; money = money })) ∷ []) + select-decision : MessageFilter Buyer1Interface + select-decision (Msg (S (S (S Z))) _) = true + select-decision _ = false + wait-for-decision : ∀ {i Γ} → + ∞ActorM i Buyer1Interface (Lift AgreeChoice) Γ (λ _ → Γ) + wait-for-decision = do + record {msg = Msg (S (S (S Z))) (ac ∷ []) } ← (selective-receive select-decision) + where + record { msg = (Msg Z _) ; msg-ok = () } + record { msg = (Msg (S Z) _) ; msg-ok = () } + record { msg = (Msg (S (S Z)) _) ; msg-ok = () } + record { msg = (Msg (S (S (S (S _)))) _) ; msg-ok = () } + return ac + + +-- ========= +-- BUYER 2 +-- ========= + +buyer2 : ∀ {i} → ActorM i Buyer2Interface ⊤₁ [] (λ _ → []) +buyer2 = begin do + wait-for-seller + wait-for-buyer1 + lift contribution ← wait-for-contribution + handle-contribution (S Z) Z contribution + strengthen [] + where + select-seller : MessageFilter Buyer2Interface + select-seller (Msg Z _) = true + select-seller (Msg (S _) _) = false + wait-for-seller : ∀ {i Γ} → ∞ActorM i Buyer2Interface ⊤₁ Γ (λ _ → Buyer2-to-Seller ∷ Γ) + wait-for-seller = do + record { msg = Msg Z _ } ← (selective-receive select-seller) + where + record { msg = (Msg (S _) _) ; msg-ok = () } + return _ + select-buyer1 : MessageFilter Buyer2Interface + select-buyer1 (Msg (S Z) _) = true + select-buyer1 _ = false + wait-for-buyer1 : ∀ {i Γ} → ∞ActorM i Buyer2Interface ⊤₁ Γ (λ _ → Buyer2-to-Buyer1 ∷ Γ) + wait-for-buyer1 = do + record {msg = Msg (S Z) _ } ← selective-receive select-buyer1 + where + record { msg = (Msg Z _) ; msg-ok = () } + record { msg = (Msg (S (S _)) _) ; msg-ok = () } + return _ + select-contribution : MessageFilter Buyer2Interface + select-contribution (Msg (S (S Z)) _) = true + select-contribution _ = false + wait-for-contribution : ∀ {i Γ} → ∞ActorM i Buyer2Interface (Lift Contribution) Γ (λ _ → Γ) + wait-for-contribution = do + record { msg = Msg (S (S Z)) (cc ∷ []) } ← (selective-receive select-contribution) + where + record { msg = (Msg Z _) ; msg-ok = () } + record { msg = (Msg (S Z) _) ; msg-ok = () } + record { msg = (Msg (S (S (S _))) _) ; msg-ok = () } + return cc + contribution-is-fair : Money → Money → Bool + contribution-is-fair price money = ⌊ price ∸ money ≤? money ⌋ + handle-contribution : ∀ {i Γ} → + Γ ⊢ Buyer2-to-Seller → + Γ ⊢ Buyer2-to-Buyer1 → + Contribution → + ∞ActorM i Buyer2Interface ⊤₁ Γ (λ _ → Γ) + handle-contribution seller buyer1 record { book = book ; money = money } with (contribution-is-fair (Book.price book) money) + ... | true = do + (buyer1 ![t: Z ] ((lift AGREE) ∷ [])) + (seller ![t: Z ] ((lift AGREE) ∷ [])) + (transfer-money seller (⊆-suc ⊆-refl) Buyer2 book ((Book.price book) ∸ money)) + ... | false = do + (buyer1 ![t: Z ] ((lift QUIT) ∷ [])) + (seller ![t: Z ] ((lift QUIT) ∷ [])) + +-- ============ +-- SUPERVISOR +-- ============ + +bookstore-supervisor : ∀ {i} → ∞ActorM i [] ⊤₁ [] (λ _ → []) +bookstore-supervisor = do + spawn seller + spawn buyer1 + spawn buyer2 + Z ![t: Z ] (([ (S (S Z)) ]>: ((S Z) ∷ ((S (S Z)) ∷ []))) ∷ []) + Z ![t: S Z ] (([ (S Z) ]>: ((S (S (S Z))) ∷ [])) ∷ []) + (S Z) ![t: Z ] (([ (S (S Z)) ]>: (Z ∷ (S (S Z) ∷ []))) ∷ []) + (S Z) ![t: S Z ] (([ Z ]>: ((S (S Z)) ∷ [])) ∷ []) + (strengthen []) + diff --git a/src/Selective/Examples/Call.lagda.tex b/src/Selective/Examples/Call.lagda.tex index 75eadbb..b92c039 100644 --- a/src/Selective/Examples/Call.lagda.tex +++ b/src/Selective/Examples/Call.lagda.tex @@ -17,6 +17,7 @@ ) open import Data.Unit using (⊤ ; tt) open import Relation.Nullary using (yes ; no) +open import Relation.Nullary.Decidable using (⌊_⌋) open SelectedMessage @@ -28,9 +29,7 @@ All receive-field-content MT → (ValueType UniqueTag ∷ MtIn) ∈ IS → Bool -call-select-unwrap tag Z (tag' ∷ fs) Z with (tag ≟ tag') -... | yes p = true -... | no p = false +call-select-unwrap tag Z (tag' ∷ fs) Z = ⌊ tag ≟ tag' ⌋ call-select-unwrap _ Z _ (S p) = false call-select-unwrap _ (S x) _ Z = false call-select-unwrap tag (S x) fs (S p) = call-select-unwrap tag x fs p @@ -62,7 +61,7 @@ The actor that we're calling must accept a message containing the unique tag and a reference. There are no further constraints on the additional fields \AgdaBound{MtTo}. \begin{code} - ((ValueType UniqueTag ∷ ReferenceType IS' ∷ MtTo) ∈ To) → + ((ValueType UniqueTag ∷ ReferenceType IS' ∷ MtTo) ∈ To) → \end{code} The caller must supply the unique tag manually, but it would be easy to extend the actor monad with some state that can provide unique tags automatically. diff --git a/src/Selective/Examples/Call2.agda b/src/Selective/Examples/Call2.agda new file mode 100644 index 0000000..254c0c2 --- /dev/null +++ b/src/Selective/Examples/Call2.agda @@ -0,0 +1,98 @@ +module Selective.Examples.Call2 where + +open import Selective.ActorMonad public +open import Selective.Examples.Channel public +open import Data.List using (List ; _∷_ ; [] ; _++_ ; map) +open import Data.List.All using (All ; _∷_ ; []) renaming (map to ∀map) +open import Data.Bool using (Bool ; if_then_else_ ; false ; true) +open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; _≟_ ) +open import Size +open import Level using (Lift ; lift) renaming (zero to lzero ; suc to lsuc) +open import Data.List.Any using (here ; there) +open import Relation.Binary.PropositionalEquality + using (_≡_ ; refl ; cong ; sym ; inspect ; [_] ; trans) +open import Membership using ( + _∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] + ; ⊆-refl ; ⊆-trans ; ⊆-suc ; translate-⊆ + ; lookup-all + ) +open import Data.Unit using (⊤ ; tt) +open import Relation.Nullary using (yes ; no) +open import Relation.Nullary.Decidable using (⌊_⌋) +open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) + +open ChannelType +open ChannelInitiation + +call : ∀ {Γ i caller} → + ∀ protocol → + Request Γ caller protocol → + ∞ActorM i caller (Message (protocol .response .channel-shape)) Γ (add-references Γ) +call protocol request = + let + open ChannelInitiationSession + open Request + open ChannelSession + in do + initiate-channel _ request + let rs = request .session .response-session + from-channel (protocol .response) rs + +CalculatorResponse : InboxShape +CalculatorResponse = ( + ValueType UniqueTag ∷ + ValueType ℕ ∷ []) ∷ [] + +Calculator : InboxShape +Calculator = ( + ValueType UniqueTag ∷ + ReferenceType CalculatorResponse ∷ + ValueType ℕ ∷ + ValueType ℕ ∷ [] + ) ∷ [] + +CalculatorProtocol : ChannelInitiation +CalculatorProtocol = record + { request = Calculator + ; response = record { + channel-shape = CalculatorResponse + ; all-tagged = (HasTag _) ∷ [] + } + ; request-tagged = (HasTag+Ref (ValueType ℕ ∷ ValueType ℕ ∷ [])) ∷ [] + } + +calculatorActor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → []) +calculatorActor .force = receive ∞>>= λ { + (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) .force → + (Z ![t: Z ] ((lift tag) ∷ (lift (n + m)) ∷ [])) ∞>> (do + strengthen [] + calculatorActor) + ; (Msg (S ()) _) + } + +TestBox : InboxShape +TestBox = ( + ValueType UniqueTag ∷ + ValueType ℕ ∷ []) ∷ + [] ∷ [] + +calltestActor : ∀{i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → []) +calltestActor = do + (spawn∞ calculatorActor) + Msg Z (tag ∷ n ∷ []) ← call CalculatorProtocol (record { + var = Z + ; chosen-field = Z + ; fields = (lift 32) ∷ ((lift 10) ∷ []) + ; session = record { + can-request = ⊆-refl + ; response-session = record { + can-receive = Z ∷ [] + ; tag = 0 + } + } + }) + where + Msg (S ()) _ + (strengthen []) + (return n) + diff --git a/src/Selective/Examples/Channel.agda b/src/Selective/Examples/Channel.agda new file mode 100644 index 0000000..a3010ad --- /dev/null +++ b/src/Selective/Examples/Channel.agda @@ -0,0 +1,224 @@ +module Selective.Examples.Channel where + +open import Selective.ActorMonad public +open import Data.List using (List ; _∷_ ; [] ; _++_ ; map) +open import Data.List.All using (All ; _∷_ ; []) renaming (map to ∀map) +open import Data.Bool using (Bool ; if_then_else_ ; false ; true) +open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; _≟_ ) +open import Size +open import Level using (Lift ; lift) renaming (zero to lzero ; suc to lsuc) +open import Data.List.Any using (here ; there) +open import Relation.Binary.PropositionalEquality + using (_≡_ ; refl ; cong ; sym ; inspect ; [_] ; trans) +open import Membership using ( + _∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] + ; ⊆-refl ; ⊆-trans ; ⊆-suc ; translate-⊆ + ; lookup-all + ) +open import Data.Unit using (⊤ ; tt) +open import Relation.Nullary using (yes ; no) +open import Relation.Nullary.Decidable using (⌊_⌋) +open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) + +UniqueTag = ℕ +TagField = ValueType UniqueTag + +data IsChannelMessage : MessageType → Set₁ where + HasTag : ∀ MT → IsChannelMessage (TagField ∷ MT) + +record ChannelType : Set₁ where + field + channel-shape : InboxShape + all-tagged : All IsChannelMessage channel-shape + +open ChannelType + +record ChannelSession (channel : ChannelType) (receiver : InboxShape): Set₁ where + field + can-receive : (channel .channel-shape) <: receiver + tag : UniqueTag + +record ChannelCandidate (channel-shape receiver : InboxShape) : Set₁ where + field + MT : MessageType + channel-pointer : MT ∈ channel-shape + receiver-pointer : MT ∈ receiver + MT-tagged : IsChannelMessage MT + +candidates-suc : ∀ {channel-shape x xs} → List (ChannelCandidate channel-shape xs) → List (ChannelCandidate (x ∷ channel-shape) xs) +candidates-suc [] = [] +candidates-suc (x ∷ candidates) = + let rec = candidates-suc candidates + open ChannelCandidate + in record + { MT = x .MT + ; channel-pointer = S (x .channel-pointer) + ; receiver-pointer = x .receiver-pointer + ; MT-tagged = x .MT-tagged + } ∷ rec + +channel-candidates : {channel-shape receiver : InboxShape} → All IsChannelMessage channel-shape → channel-shape <: receiver → List (ChannelCandidate channel-shape receiver) +channel-candidates [] sub = [] +channel-candidates (px ∷ icm) (p ∷ sub) = + let rec = channel-candidates icm sub + candidate = record + { MT = _ + ; channel-pointer = Z + ; receiver-pointer = p + ; MT-tagged = px + } + in candidate ∷ candidates-suc rec + +data DecideAccept : {MT CT : MessageType} {caller : InboxShape} → + UniqueTag → + MT ∈ caller → + CT ∈ caller → + IsChannelMessage CT → + All receive-field-content MT → + Set₁ where + Acceptable : ∀ {MT caller tag} {rest : All receive-field-content MT} {p : (TagField ∷ MT) ∈ caller} → DecideAccept tag p p (HasTag MT) (tag ∷ rest) + Unacceptable : ∀ {MT CT caller tag} {p : MT ∈ caller} {q : CT ∈ caller} {irp : IsChannelMessage CT} {fields : All receive-field-content MT} → DecideAccept tag p q irp fields + +accept-response-candidate : {MT CT : MessageType} {receiver : InboxShape} → + (tag : UniqueTag) → + (p : MT ∈ receiver) → + (q : CT ∈ receiver) → + (irp : IsChannelMessage CT) → + (fields : All receive-field-content MT) → + DecideAccept tag p q irp fields +accept-response-candidate tag Z Z (HasTag MT) (tag' ∷ fields) with (tag ≟ tag') +... | (yes refl) = Acceptable +... | (no _) = Unacceptable +accept-response-candidate tag Z (S q) irm fields = Unacceptable +accept-response-candidate tag (S p) Z irm fields = Unacceptable +accept-response-candidate tag (S p) (S q) irm fields with (accept-response-candidate tag p q irm fields) +... | Acceptable = Acceptable +... | Unacceptable = Unacceptable + +open ChannelCandidate + +accept-response-unwrapped : {MT : MessageType} {channel-shape receiver : InboxShape} → + UniqueTag → + MT ∈ receiver → + All receive-field-content MT → + List (ChannelCandidate channel-shape receiver) → + Bool +accept-response-unwrapped tag p fields [] = false +accept-response-unwrapped tag p fields (candidate ∷ candidates) with (accept-response-candidate tag p (candidate .receiver-pointer) (candidate .MT-tagged) fields) +... | Acceptable = true +... | Unaceptable = accept-response-unwrapped tag p fields candidates + + +accept-response : ∀ {ct receiver} → ChannelSession ct receiver → MessageFilter receiver +accept-response {ct} {receiver} session (Msg x fields) = + let + open ChannelType + open ChannelSession + candidates = channel-candidates (ct .all-tagged) (session .can-receive) + in accept-response-unwrapped (session .tag) x fields candidates + +record ChannelMessageDependent (channel-shape : InboxShape) (accepted-type : MessageType) : Set₁ where + field + accepted-which : accepted-type ∈ channel-shape + fields : All receive-field-content accepted-type + +convert-response-unwrapped : {MT : MessageType} {channel-shape receiver : InboxShape} → + (tag : UniqueTag) → + (x : MT ∈ receiver) → + (fields : All receive-field-content MT) → + (candidates : List (ChannelCandidate channel-shape receiver)) → + (ok : accept-response-unwrapped tag x fields candidates ≡ true) → + ChannelMessageDependent channel-shape MT +convert-response-unwrapped tag x fields [] () +convert-response-unwrapped tag x fields (candidate ∷ candidates) ok with (accept-response-candidate tag x (candidate .receiver-pointer) (candidate .MT-tagged) fields) +... | Acceptable = record { accepted-which = candidate .channel-pointer ; fields = fields } +... | Unacceptable = convert-response-unwrapped tag x fields candidates ok + + +convert-response : ∀ {ct receiver} {session : ChannelSession ct receiver} → + (sm : SelectedMessage (accept-response session)) → ChannelMessageDependent (ct .channel-shape) (selected-type sm) +convert-response {ct} {session = session} record { msg = (Msg x fields) ; msg-ok = msg-ok } = + let + open ChannelType + open ChannelSession + candidates = channel-candidates (ct .all-tagged) (session .can-receive) + in convert-response-unwrapped (session .tag) x fields candidates msg-ok + +from-channel : ∀ {Γ i receiver} → + ∀ ct → + ChannelSession ct receiver → + ∞ActorM i receiver (Message (ct .channel-shape)) Γ (add-references Γ) +from-channel ct cs = + let + open ChannelType + open ChannelSession + open Message + in do + m@record { msg = msg ; msg-ok = msg-ok } ← selective-receive (accept-response cs) + let record { accepted-which = aw ; fields = fields } = convert-response {session = cs} m + return₁ (Msg {MT = msg .MT} aw fields) + + +data IsRequestMessage (IS : InboxShape) : MessageType → Set₁ where + HasTag+Ref : ∀ MT → IsRequestMessage IS (TagField ∷ ReferenceType IS ∷ MT) + +record ChannelInitiation : Set₁ where + field + request : InboxShape + response : ChannelType + request-tagged : All (IsRequestMessage (response .channel-shape)) request + +open ChannelInitiation + +record ChannelInitiationSession (ci : ChannelInitiation) (caller callee : InboxShape): Set₁ where + field + can-request : (ci .request) <: callee + response-session : ChannelSession (ci .response) caller + +extra-fields-shape : ∀ {IS Mt} → IsRequestMessage IS Mt → MessageType +extra-fields-shape (HasTag+Ref Mt) = Mt + +extra-fields : ∀ {IS Mt} → (Γ : TypingContext) → IsRequestMessage IS Mt → Set₁ +extra-fields Γ irm = All (send-field-content Γ) (extra-fields-shape irm) + +record Request (Γ : TypingContext) (caller : InboxShape) (ci : ChannelInitiation) : Set₁ where + field + {callee} : InboxShape + var : Γ ⊢ callee + {MtTo} : MessageType + chosen-field : MtTo ∈ (ci .request) + fields : extra-fields Γ (lookup-all chosen-field (ci .request-tagged)) + session : ChannelInitiationSession ci caller callee + +suc-send-field-content : ∀ {Γ IS F} → send-field-content Γ F → send-field-content (IS ∷ Γ) F +suc-send-field-content {F = ValueType x} sfc = sfc +suc-send-field-content {F = ReferenceType x} ([ actual-is-sendable ]>: actual-handles-requested) = [ S actual-is-sendable ]>: actual-handles-requested + +initiate-channel-fields : + ∀ {Γ caller ci} → + (request : Request Γ caller ci) → + All (send-field-content (caller ∷ Γ)) (Request.MtTo request) +initiate-channel-fields {ci = ci} record { + chosen-field = chosen-field + ; fields = fields + ; session = session + } with (lookup-all chosen-field (ci .request-tagged)) +... | HasTag+Ref _ = + let open ChannelSession + open ChannelInitiationSession + channel = session .response-session + in (lift (channel .tag)) ∷ (([ Z ]>: (channel .can-receive)) ∷ ∀map suc-send-field-content fields) + +initiate-channel : ∀ {Γ i receiver} → + ∀ ci → + Request Γ receiver ci → + ∞ActorM i receiver ⊤₁ Γ (λ _ → Γ) +initiate-channel ci request = + let + open Request + open ChannelInitiationSession + in do + self + let protocol-to-callee = translate-⊆ (request .session .can-request) + S (request .var) ![t: protocol-to-callee (request .chosen-field) ] initiate-channel-fields request + strengthen (⊆-suc ⊆-refl) diff --git a/src/Selective/Examples/Chat.agda b/src/Selective/Examples/Chat.agda new file mode 100644 index 0000000..b428a13 --- /dev/null +++ b/src/Selective/Examples/Chat.agda @@ -0,0 +1,608 @@ +module Selective.Examples.Chat where + +open import Selective.ActorMonad public +open import Selective.Examples.Call using (UniqueTag ; call) +open import Data.List using (List ; _∷_ ; [] ; map ; _++_ ; reverse ; _∷ʳ_ ; length) +open import Data.List.All using (All ; _∷_ ; []) +open import Data.Bool using (Bool ; false ; true) +open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; _≟_ ; pred) +open import Data.Maybe as Maybe using (Maybe ; just ; nothing) +open import Data.String using (String) renaming (_++_ to _||_) +open import Size +open import Level using (Lift ; lift) renaming (zero to lzero ; suc to lsuc) +open import Data.List.Any using (here ; there) +open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong) +open import Relation.Nullary using (yes ; no) +open import Relation.Nullary.Decidable using (⌊_⌋) +open import Membership using (_∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] ; ⊆-refl ; ⊆-suc ; ⊆++-refl) +open import Data.Unit using (⊤ ; tt) + +open import Data.List.Properties + +open import Category.Monad + +open import Debug +open import Data.Nat.Show using (show) + +RoomName = ℕ +ClientName = ℕ + +ClientInterface : InboxShape +Client-to-Room : InboxShape +Room-to-Client : InboxShape + +-- ============= +-- JOIN ROOM +-- ============= + +data JoinRoomSuccess : Set where + JR-SUCCESS : RoomName → JoinRoomSuccess + +data JoinRoomFail : Set where + JR-FAIL : RoomName → JoinRoomFail + +data JoinRoomStatus : Set where + JRS-SUCCESS JRS-FAIL : RoomName → JoinRoomStatus + +JoinRoomSuccessReply : MessageType +JoinRoomSuccessReply = ValueType UniqueTag ∷ ValueType JoinRoomSuccess ∷ ReferenceType Client-to-Room ∷ [] + +JoinRoomFailReply : MessageType +JoinRoomFailReply = ValueType UniqueTag ∷ ValueType JoinRoomFail ∷ [] + +JoinRoomReplyInterface : InboxShape +JoinRoomReplyInterface = (JoinRoomSuccessReply ∷ JoinRoomFailReply ∷ []) ++ Room-to-Client + +JoinRoom : MessageType +JoinRoom = ValueType UniqueTag ∷ ReferenceType JoinRoomReplyInterface ∷ ValueType RoomName ∷ ValueType ClientName ∷ [] + +-- ============= +-- CREATE ROOM +-- ============= + +data CreateRoomResult : Set where + CR-SUCCESS CR-EXISTS : RoomName → CreateRoomResult + +CreateRoomReply : MessageType +CreateRoomReply = ValueType UniqueTag ∷ ValueType CreateRoomResult ∷ [] + +CreateRoom : MessageType +CreateRoom = ValueType UniqueTag ∷ ReferenceType (CreateRoomReply ∷ []) ∷ ValueType RoomName ∷ [] + +-- ============ +-- LIST ROOMS +-- ============ + +RoomList : Set +RoomList = List RoomName + +ListRoomsReply : MessageType +ListRoomsReply = ValueType UniqueTag ∷ ValueType RoomList ∷ [] + +ListRooms : MessageType +ListRooms = ValueType UniqueTag ∷ ReferenceType (ListRoomsReply ∷ []) ∷ [] + +-- === +-- +-- === + +Client-to-RoomManager : InboxShape +Client-to-RoomManager = JoinRoom ∷ CreateRoom ∷ ListRooms ∷ [] + +RoomManagerInterface : InboxShape +RoomManagerInterface = Client-to-RoomManager + +GetRoomManagerReply : MessageType +GetRoomManagerReply = ValueType UniqueTag ∷ ReferenceType RoomManagerInterface ∷ [] + +GetRoomManager : MessageType +GetRoomManager = ValueType UniqueTag ∷ ReferenceType (GetRoomManagerReply ∷ []) ∷ [] + +RoomSupervisorInterface : InboxShape +RoomSupervisorInterface = GetRoomManager ∷ [] + +ClientSupervisorInterface : InboxShape +ClientSupervisorInterface = + (ReferenceType RoomSupervisorInterface ∷ []) + ∷ GetRoomManagerReply + ∷ [] + + +-- +-- +-- + +record ChatMessageContent : Set where + constructor chat-from_message:_ + field + sender : ClientName + message : String + +ChatMessage : MessageType +ChatMessage = ValueType ChatMessageContent ∷ [] + +LeaveRoom : MessageType +LeaveRoom = ValueType ClientName ∷ [] + +Client-to-Room = ChatMessage ∷ LeaveRoom ∷ [] + +Room-to-Client = ChatMessage ∷ [] + +AddToRoom : MessageType +AddToRoom = ValueType ClientName ∷ ReferenceType Room-to-Client ∷ [] + +RoomManager-to-Room : InboxShape +RoomManager-to-Room = AddToRoom ∷ [] + +RoomInstanceInterface : InboxShape +RoomInstanceInterface = Client-to-Room ++ RoomManager-to-Room + +ClientInterface = (ReferenceType RoomManagerInterface ∷ []) ∷ CreateRoomReply ∷ ListRoomsReply ∷ JoinRoomReplyInterface + +-- ====== +-- ROOM +-- ====== + +ClientList : Set +ClientList = List ClientName + +record RoomState : Set₁ where + field + clients : ClientList + + +cl-to-context : ClientList → TypingContext +cl-to-context = map λ _ → Room-to-Client + +rs-to-context : RoomState → TypingContext +rs-to-context rs = let open RoomState + in cl-to-context (rs .clients) + +record RoomLeave (rs : ClientList) (name : ClientName) : Set₁ where + field + filtered : ClientList + subs : (cl-to-context filtered) ⊆ (cl-to-context rs) + +++-temp-fix : (l r : ClientList) → (x : ClientName) → (l ++ (x ∷ r)) ≡ ((l ∷ʳ x) ++ r) +++-temp-fix [] r x = refl +++-temp-fix (x₁ ∷ l) r x = cong (_∷_ x₁) (++-temp-fix l r x) + +room-instance : ∀ {i} → ActorM i RoomInstanceInterface RoomState [] rs-to-context +room-instance = begin (loop (record { clients = [] })) + where + -- only removes first occurance... + leave-room : (cl : ClientList) → (name : ClientName) → RoomLeave cl name + leave-room [] name = record { filtered = [] ; subs = [] } + leave-room (x ∷ cl) name with (x ≟ name) + ... | (yes _) = record { filtered = cl ; subs = ⊆-suc ⊆-refl } + ... | (no _) = let + rl = leave-room cl name + open RoomLeave + in record { filtered = x ∷ rl .filtered ; subs = Z ∷ ⊆-suc (rl .subs) } + send-to-others : ∀ {i} → (cl : ClientList) → + ClientName → + String → + ∞ActorM i RoomInstanceInterface ⊤₁ (cl-to-context cl) (λ _ → cl-to-context cl) + send-to-others [] _ _ = return _ + send-to-others cl@(_ ∷ _) name message = send-loop [] cl + where + build-pointer : (l r : ClientList) → + cl-to-context r ⊢ Room-to-Client → + (cl-to-context (l ++ r)) ⊢ Room-to-Client + build-pointer [] r p = p + build-pointer (x ∷ l) r p = S (build-pointer l r p) + recurse : ∀ {i} → (l r : ClientList) → (x : ClientName) → + ∞ActorM i RoomInstanceInterface ⊤₁ (cl-to-context (l ++ (x ∷ r))) (λ _ → (cl-to-context (l ++ (x ∷ r)))) + send-loop : ∀ {i} → (l r : ClientList) → + ∞ActorM i RoomInstanceInterface ⊤₁ (cl-to-context (l ++ r)) (λ _ → cl-to-context (l ++ r)) + send-loop l [] = return _ + send-loop l (x ∷ r) with (x ≟ name) + ... | (yes _) = recurse l r x + ... | (no _) = let p = build-pointer l (x ∷ r) Z + in debug ("Sending to " || show x || ": " || message) (p ![t: Z ] (((lift (chat-from name message: message)) ∷ []))) >> recurse l r x + recurse l r x rewrite ++-temp-fix l r x = send-loop (l ∷ʳ x) r + handle-message : ∀ {i} → (rs : RoomState) → + (m : Message RoomInstanceInterface) → + ∞ActorM i RoomInstanceInterface RoomState (add-references (rs-to-context rs) m) rs-to-context + -- chat message + handle-message rs (Msg Z (chat-from client-name message: message ∷ [])) = do + let open RoomState + debug ("room sending " || show (pred (length (rs .clients))) || " messages from " || show client-name || ": " || message) (send-to-others (rs .clients) client-name message) + (return₁ rs) + -- leave room + handle-message rs (Msg (S Z) (client-name ∷ [])) = do + let + open RoomState + open RoomLeave + rl = leave-room (rs .clients) client-name + debug ("client#" || show client-name || " left the room") (strengthen (rl .subs)) + (return₁ (record { clients = rl .filtered })) + -- add to room + handle-message rs (Msg (S (S Z)) (client-name ∷ _ ∷ [])) = do + let open RoomState + return₁ (record { clients = client-name ∷ rs .clients }) + handle-message rs (Msg (S (S (S ()))) _) + loop : ∀ {i} → + (rs : RoomState) → + ∞ActorM i RoomInstanceInterface RoomState (rs-to-context rs) rs-to-context + loop state .force = begin do + m ← debug ("ROOM LOOP") receive + state' ← (handle-message state m) + loop state' + +-- ============== +-- ROOM MANAGER +-- ============== + +record RoomManagerState : Set₁ where + field + rooms : RoomList + +rms-to-context : RoomManagerState → TypingContext +rms-to-context rms = rl-to-context (rms .rooms) + where + open RoomManagerState + rl-to-context : RoomList → TypingContext + rl-to-context = map λ _ → RoomInstanceInterface + +lookup-room : ∀ {i} → {Γ : TypingContext} → + (rms : RoomManagerState) → + RoomName → + ∞ActorM i RoomManagerInterface (Maybe ((Γ ++ (rms-to-context rms)) ⊢ RoomInstanceInterface)) (Γ ++ (rms-to-context rms)) (λ _ → Γ ++ (rms-to-context rms)) +lookup-room rms name = + let open RoomManagerState + in return₁ (loop _ (rms .rooms)) + where + rl-to-context : RoomList → TypingContext + rl-to-context = map λ _ → RoomInstanceInterface + loop : (Γ : TypingContext) → (rl : RoomList) → Maybe ((Γ ++ rl-to-context rl) ⊢ RoomInstanceInterface) + loop [] [] = nothing + loop [] (x ∷ xs) with (x ≟ name) + ... | (yes p) = just Z + ... | (no _) = RawMonad._>>=_ Maybe.monad (loop [] xs) λ p → just (S p) + loop (x ∷ Γ) rl = RawMonad._>>=_ Maybe.monad (loop Γ rl) (λ p → just (S p)) + +room-manager : ∀ {i} → ActorM i RoomManagerInterface RoomManagerState [] rms-to-context +room-manager = begin (loop (record { rooms = [] })) + where + handle-room-join : ∀ {i} → {Γ : TypingContext} → + UniqueTag → + RoomName → + ClientName → + (Γ ⊢ JoinRoomReplyInterface) → + (Maybe (Γ ⊢ RoomInstanceInterface)) → + ∞ActorM i RoomManagerInterface ⊤₁ Γ (λ _ → Γ) + handle-room-join tag room-name client-name cp (just rp) = do + cp ![t: Z ] ((lift tag) ∷ ((lift (JR-SUCCESS room-name)) ∷ (([ rp ]>: (Z ∷ ((S Z) ∷ []))) ∷ []))) + rp ![t: S (S Z) ] (lift client-name ∷ ([ cp ]>: ((S (S Z)) ∷ [])) ∷ []) + handle-room-join tag room-name client-name p nothing = + p ![t: S Z ] (lift tag ∷ (lift (JR-FAIL room-name) ∷ [])) + handle-create-room : ∀ {i} → + (rms : RoomManagerState) → + UniqueTag → + RoomName → + Maybe (((CreateRoomReply ∷ []) ∷ rms-to-context rms) ⊢ RoomInstanceInterface) → + ∞ActorM i RoomManagerInterface RoomManagerState ((CreateRoomReply ∷ []) ∷ rms-to-context rms) rms-to-context + handle-create-room rms tag name (just x) = do + (Z ![t: Z ] ((lift tag) ∷ ((lift (CR-EXISTS name)) ∷ []))) + (strengthen (⊆-suc ⊆-refl)) + (return₁ rms) + handle-create-room rms tag name nothing = do + (Z ![t: Z ] ((lift tag) ∷ ((lift (CR-SUCCESS name)) ∷ []))) + (strengthen (⊆-suc ⊆-refl)) + spawn room-instance + let + rms' : RoomManagerState + rms' = (record { rooms = name ∷ RoomManagerState.rooms rms }) + (return₁ rms') + handle-message : ∀ {i} → (rms : RoomManagerState) → + (m : Message RoomManagerInterface) → + ∞ActorM i RoomManagerInterface RoomManagerState (add-references (rms-to-context rms) m) rms-to-context + -- Jooin room + handle-message state (Msg Z (tag ∷ _ ∷ room-name ∷ client-name ∷ [])) = do + p ← (lookup-room state room-name) + handle-room-join tag room-name client-name Z p + (strengthen (⊆-suc ⊆-refl)) + (return₁ state) + -- Create room + handle-message state (Msg (S Z) (tag ∷ _ ∷ name ∷ [])) = do + p ← lookup-room state name + handle-create-room state tag name p + -- List rooms + handle-message state (Msg (S (S Z)) (tag ∷ _ ∷ [])) = do + (Z ![t: Z ] ((lift tag) ∷ (lift (RoomManagerState.rooms state) ∷ []))) + (strengthen (⊆-suc ⊆-refl)) + (return₁ state) + handle-message state (Msg (S (S (S ()))) _) + loop : ∀ {i} → + (rms : RoomManagerState) → + ∞ActorM i RoomManagerInterface RoomManagerState (rms-to-context rms) rms-to-context + loop state .force = begin do + m ← receive + state' ← handle-message state m + loop state' + +-- ================= +-- ROOM SUPERVISOR +-- ================= + +rs-context : TypingContext +rs-context = RoomManagerInterface ∷ [] + +-- room-supervisor spawns the room-manager +-- and provides an interface for getting a reference to the current room-manager +-- we don't ever change that instance, but we could if we want +room-supervisor : ∀ {i} → ActorM i RoomSupervisorInterface ⊤₁ [] (λ _ → rs-context) +room-supervisor = begin do + (spawn room-manager) + provide-manager-instance + where + provide-manager-instance : ∀ {i} → ∞ActorM i RoomSupervisorInterface ⊤₁ rs-context (λ _ → rs-context) + provide-manager-instance .force = begin do + (Msg Z (tag ∷ _ ∷ [])) ← receive + where (Msg (S ()) _) + (Z ![t: Z ] (lift tag ∷ (([ (S Z) ]>: ⊆-refl) ∷ []))) + (strengthen (⊆-suc ⊆-refl)) + provide-manager-instance + +-- ================ +-- CLIENT GENERAL +-- ================ + +busy-wait : ∀ {i IS Γ} → ℕ → ∞ActorM i IS ⊤₁ Γ (λ _ → Γ) +busy-wait zero = return _ +busy-wait (suc n) = return tt >> busy-wait n + +client-get-room-manager : ∀ {i} → ∞ActorM i ClientInterface ⊤₁ [] (λ _ → RoomManagerInterface ∷ []) +client-get-room-manager = do + record { msg = Msg Z _} ← (selective-receive (λ { + (Msg Z x₁) → true + ; (Msg (S _) _) → false + })) + where + record { msg = (Msg (S _) _) ; msg-ok = ()} + return _ + +client-create-room : ∀ {i } → + {Γ : TypingContext} → + Γ ⊢ RoomManagerInterface → + UniqueTag → + RoomName → + ∞ActorM i ClientInterface (Lift CreateRoomResult) Γ (λ _ → Γ) +client-create-room p tag name = do + record { msg = (Msg (S Z) (_ ∷ cr ∷ [])) } ← (call p (S Z) tag ((lift name) ∷ []) ((S Z) ∷ []) Z) + where + record { msg = (Msg Z (_ ∷ _)) ; msg-ok = () } + record { msg = (Msg (S (S _)) _) ; msg-ok = () } + return cr + +add-if-join-success : TypingContext → + Lift {lzero} {lsuc lzero} JoinRoomStatus → + TypingContext +add-if-join-success Γ (lift (JRS-SUCCESS x)) = Client-to-Room ∷ Γ +add-if-join-success Γ (lift (JRS-FAIL x)) = Γ + +client-join-room : ∀ {i Γ} → + Γ ⊢ RoomManagerInterface → + UniqueTag → + RoomName → + ClientName → + ∞ActorM i ClientInterface (Lift JoinRoomStatus) Γ (add-if-join-success Γ) +client-join-room p tag room-name client-name = do + self + S p ![t: Z ] ((lift tag) ∷ (([ Z ]>: ⊆-suc (⊆-suc (⊆-suc ⊆-refl))) ∷ (lift room-name) ∷ ((lift client-name) ∷ []))) + (strengthen (⊆-suc ⊆-refl)) + m ← (selective-receive (select-join-reply tag)) + handle-message m + where + select-join-reply : UniqueTag → MessageFilter ClientInterface + select-join-reply tag (Msg Z _) = false + select-join-reply tag (Msg (S Z) _) = false + select-join-reply tag (Msg (S (S Z)) _) = false + select-join-reply tag (Msg (S (S (S Z))) (tag' ∷ _)) = ⌊ tag ≟ tag' ⌋ + select-join-reply tag (Msg (S (S (S (S Z)))) (tag' ∷ _)) = ⌊ tag ≟ tag' ⌋ + select-join-reply tag (Msg (S (S (S (S (S Z))))) x₁) = false + select-join-reply tag (Msg (S (S (S (S (S (S ())))))) _) + handle-message : ∀ {tag i Γ} → (m : SelectedMessage (select-join-reply tag)) → + ∞ActorM i ClientInterface (Lift JoinRoomStatus) + (add-selected-references Γ m) (add-if-join-success Γ) + handle-message record { msg = (Msg Z _) ; msg-ok = () } + handle-message record { msg = (Msg (S Z) _) ; msg-ok = () } + handle-message record { msg = (Msg (S (S Z)) _) ; msg-ok = () } + handle-message record { msg = (Msg (S (S (S Z))) (_ ∷ JR-SUCCESS room-name ∷ _ ∷ [])) } = return (JRS-SUCCESS room-name) + handle-message record { msg = (Msg (S (S (S (S Z)))) (_ ∷ JR-FAIL room-name ∷ [])) } = return (JRS-FAIL room-name) + handle-message record { msg = (Msg (S (S (S (S (S Z))))) _) ; msg-ok = () } + handle-message record { msg = (Msg (S (S (S (S (S (S ())))))) _) } + +client-send-message : ∀ {i Γ} → + Γ ⊢ Client-to-Room → + ClientName → + String → + ∞ActorM i ClientInterface ⊤₁ Γ (λ _ → Γ) +client-send-message p client-name message = p ![t: Z ] ((lift (chat-from client-name message: message)) ∷ []) + +client-receive-message : ∀ {i Γ} → + ∞ActorM i ClientInterface (Lift ChatMessageContent) Γ (λ _ → Γ) +client-receive-message = do + m ← (selective-receive select-message) + handle-message m + where + select-message : MessageFilter ClientInterface + select-message (Msg (S (S (S (S (S Z))))) _) = true + select-message (Msg _ _) = false + handle-message : ∀ {i Γ} → (m : SelectedMessage select-message) → + ∞ActorM i ClientInterface (Lift ChatMessageContent) (add-selected-references Γ m) (λ _ → Γ) + handle-message record { msg = (Msg Z _) ; msg-ok = () } + handle-message record { msg = (Msg (S Z) _) ; msg-ok = () } + handle-message record { msg = (Msg (S (S Z)) _) ; msg-ok = () } + handle-message record { msg = (Msg (S (S (S Z))) x₁) ; msg-ok = () } + handle-message record { msg = (Msg (S (S (S (S Z)))) _) ; msg-ok = () } + handle-message record { msg = (Msg (S (S (S (S (S Z))))) (m ∷ [])) ; msg-ok = _ } = return m + handle-message record { msg = (Msg (S (S (S (S (S (S ())))))) _) } + +client-leave-room : ∀ {i Γ} → + Γ ⊢ Client-to-Room → + ClientName → + ∞ActorM i ClientInterface ⊤₁ Γ (λ _ → Γ) +client-leave-room p name = p ![t: S Z ] ((lift name) ∷ []) + +debug-chat : {a : Level} {A : Set a} → ClientName → ChatMessageContent → A → A +debug-chat client-name content = let open ChatMessageContent + in debug ("client#" || show client-name || " received \"" || content .message || "\" from client#" || show (content .sender)) + +-- ========== +-- CLIENT 1 +-- ========== + +room1-2 = 1 +room2-3 = 2 +room3-1 = 3 +room1-2-3 = 4 +name1 = 1 + +client1 : ∀ {i} → ActorM i ClientInterface ⊤₁ [] (λ _ → []) +client1 = begin do + client-get-room-manager + _ ← (client-create-room Z 0 room1-2) + _ ← (client-create-room Z 1 room3-1) + _ ← (client-create-room Z 2 room1-2-3) + lift (JRS-SUCCESS joined-room) ← (client-join-room Z 3 room3-1 name1) + where + (lift (JRS-FAIL failed-room)) → strengthen [] + lift (JRS-SUCCESS joined-room) ← (client-join-room (S Z) 4 room1-2 name1) + where + (lift (JRS-FAIL failed-room)) → strengthen [] + lift (JRS-SUCCESS joined-room) ← (client-join-room (S (S Z)) 5 room1-2-3 name1) + where + (lift (JRS-FAIL failed-room)) → strengthen [] + busy-wait 100 + (client-send-message (S Z) name1 "hi from 1 to 2") + (client-send-message Z name1 "hi from 1 to 2-3") + let open ChatMessageContent + lift m1 ← client-receive-message + lift m2 ← debug-chat name1 m1 client-receive-message + lift m3 ← debug-chat name1 m2 client-receive-message + debug-chat name1 m3 (client-send-message Z name1 "hi1 from 1 to 2-3") + (client-send-message Z name1 "hi2 from 1 to 2-3") + (client-send-message Z name1 "hi3 from 1 to 2-3") + client-leave-room (S Z) name1 + client-leave-room (Z) name1 + (strengthen []) + +-- ========== +-- CLIENT 2 +-- ========== + +name2 = 2 + +client2 : ∀ {i} → ActorM i ClientInterface ⊤₁ [] (λ _ → []) +client2 = begin do + client-get-room-manager + _ ← (client-create-room Z 0 room1-2) + _ ← (client-create-room Z 1 room2-3) + _ ← (client-create-room Z 2 room1-2-3) + lift (JRS-SUCCESS joined-room) ← (client-join-room Z 3 room1-2 name2) + where + (lift (JRS-FAIL failed-room)) → strengthen [] + lift (JRS-SUCCESS joined-room) ← (client-join-room (S Z) 4 room2-3 name2) + where + (lift (JRS-FAIL failed-room)) → strengthen [] + lift (JRS-SUCCESS joined-room) ← (client-join-room (S (S Z)) 5 room1-2-3 name2) + where + (lift (JRS-FAIL failed-room)) → strengthen [] + busy-wait 100 + debug "client2 send message" (client-send-message (S Z) name2 "hi from 2 to 3") + debug "client2 send message" (client-send-message Z name2 "hi from 2 to 1-3") + let open ChatMessageContent + lift m1 ← client-receive-message + lift m2 ← debug-chat name2 m1 client-receive-message + lift m3 ← debug-chat name2 m2 client-receive-message + client-leave-room (S Z) name2 + client-leave-room (Z) name2 + debug-chat name2 m3 (strengthen []) + +-- ========== +-- CLIENT 3 +-- ========== + +name3 = 3 + +client3 : ∀ {i} → ActorM i ClientInterface ⊤₁ [] (λ _ → []) +client3 = begin do + client-get-room-manager + _ ← (client-create-room Z 0 room2-3) + _ ← (client-create-room Z 1 room3-1) + _ ← (client-create-room Z 2 room1-2-3) + lift (JRS-SUCCESS joined-room) ← (client-join-room Z 3 room2-3 name3) + where + (lift (JRS-FAIL failed-room)) → strengthen [] + lift (JRS-SUCCESS joined-room) ← (client-join-room (S Z) 4 room3-1 name3) + where + (lift (JRS-FAIL failed-room)) → strengthen [] + lift (JRS-SUCCESS joined-room) ← (client-join-room (S (S Z)) 5 room1-2-3 name3) + where + (lift (JRS-FAIL failed-room)) → strengthen [] + busy-wait 100 + debug "client3 send message" (client-send-message (S Z) name3 "hi from 3 to 1") + debug "client3 send message" (client-send-message Z name3 "hi from 3 to 1-2") + let open ChatMessageContent + lift m1 ← client-receive-message + lift m2 ← debug-chat name3 m1 client-receive-message + lift m3 ← debug-chat name3 m2 client-receive-message + debug-chat name3 m3 (client-leave-room Z name3) + client-leave-room (S Z) name3 + client-leave-room Z name3 + (strengthen []) + +-- =================== +-- CLIENT SUPERVISOR +-- =================== + +cs-context : TypingContext +cs-context = RoomManagerInterface ∷ RoomSupervisorInterface ∷ [] + +client-supervisor : ∀ {i} → ActorM i ClientSupervisorInterface ⊤₁ [] (λ _ → cs-context) +client-supervisor = begin do + wait-for-room-supervisor + (get-room-manager Z 0) + spawn-clients + where + wait-for-room-supervisor : ∀ {i Γ} → ∞ActorM i ClientSupervisorInterface ⊤₁ Γ (λ _ → RoomSupervisorInterface ∷ Γ) + wait-for-room-supervisor = do + record { msg = Msg Z f } ← (selective-receive (λ { + (Msg Z _) → true + ; (Msg (S _) _) → false + })) + where + record { msg = (Msg (S _) _) ; msg-ok = () } + return _ + get-room-manager : ∀ {i Γ} → + Γ ⊢ RoomSupervisorInterface → + UniqueTag → + ∞ActorM i ClientSupervisorInterface ⊤₁ Γ (λ _ → RoomManagerInterface ∷ Γ) + get-room-manager p tag = do + record { msg = Msg (S Z) (_ ∷ _ ∷ []) } ← (call p Z tag [] (⊆-suc ⊆-refl) Z) + where + record { msg = (Msg Z (_ ∷ _)) ; msg-ok = () } + record { msg = (Msg (S (S ())) _) } + return _ + spawn-clients : ∀ {i} → ∞ActorM i ClientSupervisorInterface ⊤₁ cs-context (λ _ → cs-context) + spawn-clients = do + (spawn client1) + Z ![t: Z ] (([ S Z ]>: ⊆-refl) ∷ []) + (strengthen (⊆-suc ⊆-refl)) + (spawn client2) + Z ![t: Z ] (([ S Z ]>: ⊆-refl) ∷ []) + (strengthen (⊆-suc ⊆-refl)) + (spawn client3) + Z ![t: Z ] (([ S Z ]>: ⊆-refl) ∷ []) + (strengthen (⊆-suc ⊆-refl)) + +-- chat-supervisor is the top-most actor +-- it spawns and connects the ClientRegistry to the RoomRegistry +chat-supervisor : ∀ {i} → ∞ActorM i [] ⊤₁ [] (λ _ → []) +chat-supervisor = do + (spawn room-supervisor) + (spawn client-supervisor) + (Z ![t: Z ] (([ (S Z) ]>: ⊆-refl) ∷ [])) + (strengthen []) diff --git a/src/Selective/Examples/Fibonacci.agda b/src/Selective/Examples/Fibonacci.agda new file mode 100644 index 0000000..65587c7 --- /dev/null +++ b/src/Selective/Examples/Fibonacci.agda @@ -0,0 +1,120 @@ +module Selective.Examples.Fibonacci where + +open import Selective.ActorMonad public +open import Data.List using (List ; _∷_ ; []) +open import Data.List.All using (All ; _∷_ ; []) +open import Data.Bool using (Bool ; false ; true) +open import Data.Nat using (ℕ ; zero ; suc ; _+_) +open import Size +open import Level using (Lift ; lift) renaming (zero to lzero ; suc to lsuc) +open import Data.List.Any using (here ; there) +open import Relation.Binary.PropositionalEquality using (_≡_ ; refl) +open import Membership using (_∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] ; ⊆-refl ; ⊆-suc) +open import Data.Unit using (⊤ ; tt) + +open import Debug +open import Data.Nat.Show using (show) + +data End : Set where + END : End + +ℕ-message : MessageType +ℕ-message = ValueType ℕ ∷ [] + +End-message : MessageType +End-message = ValueType End ∷ [] + +Client-to-Server : InboxShape +Client-to-Server = ℕ-message ∷ End-message ∷ [] + +Server-to-Client : InboxShape +Server-to-Client = ℕ-message ∷ [] + + +ServerInterface : InboxShape +ServerInterface = + (ReferenceType Server-to-Client ∷ []) + ∷ Client-to-Server + +ClientInterface : InboxShape +ClientInterface = + (ReferenceType Client-to-Server ∷ []) + ∷ Server-to-Client + +ServerRefs : TypingContext +ServerRefs = Server-to-Client ∷ [] + +constServerRefs : {A : Set₁} → (A → TypingContext) +constServerRefs _ = ServerRefs + +data ServerAction : Set₁ where + Next : ℕ → ServerAction + Done : ServerAction + +server : ∀ {i} → ActorM i ServerInterface ⊤₁ [] constServerRefs +server = wait-for-client ∞>> run-fibonacci 1 + where + wait-for-client = selective-receive (λ { + (Msg Z _) → true + ; (Msg (S _) _) → false }) >>= λ { + record { msg = (Msg Z _) } → return tt + ; record { msg = (Msg (S _) _) ; msg-ok = () } } + wait-for-value : ∀ {i} → ∞ActorM i ServerInterface ServerAction ServerRefs constServerRefs + wait-for-value = selective-receive (λ { + (Msg Z _) → false + ; (Msg (S Z) _) → true + ; (Msg (S (S Z)) _) → true + ; (Msg (S (S (S ()))) x₁) }) >>= λ { + record { msg = (Msg Z _) ; msg-ok = () } + ; record { msg = (Msg (S Z) (n ∷ [])) } → return₁ (Next n) + ; record { msg = (Msg (S (S Z)) _) } → return₁ Done + ; record { msg = (Msg (S (S (S ()))) _) } + } + run-fibonacci : ℕ → ∀ {i} → ∞ActorM i ServerInterface ⊤₁ ServerRefs constServerRefs + run-fibonacci x .force = begin do + Next n ← wait-for-value + where Done → return _ + let next = x + n + (Z ![t: Z ] (lift next ∷ [])) + (run-fibonacci next) + +ClientRefs : TypingContext +ClientRefs = Client-to-Server ∷ [] + +constClientRefs : {A : Set₁} → (A → TypingContext) +constClientRefs _ = ClientRefs + +client : ∀ {i} → ActorM i ClientInterface ⊤₁ [] constClientRefs +client = wait-for-server ∞>> run 10 0 + where + wait-for-server : ∀ {i} → ∞ActorM i ClientInterface ⊤₁ [] constClientRefs + wait-for-server = selective-receive (λ { + (Msg Z _) → true + ; (Msg (S _) _) → false }) >>= λ { + record { msg = (Msg Z _) ; msg-ok = msg-ok } → return tt + ; record { msg = (Msg (S _) _) ; msg-ok = () } + } + wait-for-value : ∀ {i} → ∞ActorM i ClientInterface (Lift ℕ) ClientRefs constClientRefs + wait-for-value = do + record { msg = Msg (S Z) (n ∷ []) } ← selective-receive (λ { + (Msg Z _) → false + ; (Msg (S Z) _) → true + ; (Msg (S (S ())) _) }) + where + record { msg = (Msg Z _) ; msg-ok = () } + record { msg = (Msg (S (S ())) x₁) } + return n + run : ℕ → ℕ → ∀ {i} → ∞ActorM i ClientInterface ⊤₁ ClientRefs constClientRefs + run zero x = Z ![t: S Z ] ((lift END) ∷ []) + run (suc todo) x .force = begin do + (Z ![t: Z ] ((lift x) ∷ [])) + (lift n) ← wait-for-value + let next = x + n + run (debug (show next) todo) next + +spawner : ∀ {i} → ∞ActorM i [] ⊤₁ [] (λ _ → ClientInterface ∷ ServerInterface ∷ []) +spawner = do + (spawn server) + (spawn client) + (S Z ![t: Z ] (([ Z ]>: ⊆-suc ⊆-refl) ∷ [])) + (Z ![t: Z ] (([ S Z ]>: ⊆-suc ⊆-refl) ∷ [])) diff --git a/src/Selective/Examples/Main-generated.agda b/src/Selective/Examples/Main-generated.agda index 7fbd208..30ad3cd 100644 --- a/src/Selective/Examples/Main-generated.agda +++ b/src/Selective/Examples/Main-generated.agda @@ -1,6 +1,11 @@ module Selective.Examples.Main-generated where import Selective.Examples.PingPong as PingPong import Selective.Examples.Call as Call +import Selective.Examples.Fibonacci as Fib +import Selective.Examples.Chat as Chat +import Selective.Examples.Bookstore as Bookstore +import Selective.Examples.TestAC as TestAC + open import Selective.Runtime open import Selective.SimulationEnvironment open import Selective.ActorMonad @@ -9,5 +14,9 @@ open ∞ActorM pingpongEntry = singleton-env (PingPong.spawner .force) callEntry = singleton-env (Call.calltestActor .force) +fibEntry = singleton-env (Fib.spawner .force) +chatEntry = singleton-env (Chat.chat-supervisor .force) +bookstoreEntry = singleton-env (Bookstore.bookstore-supervisor .force) +testacEntry = singleton-env (TestAC.calculator-test-actor .force) -main = IO.run (run-env trace+actors-logger callEntry) +main = IO.run (run-env testacEntry) diff --git a/src/Selective/Examples/Main-template.agda b/src/Selective/Examples/Main-template.agda index ca42615..ad8938f 100644 --- a/src/Selective/Examples/Main-template.agda +++ b/src/Selective/Examples/Main-template.agda @@ -1,6 +1,11 @@ module Selective.Examples.Main-generated where import Selective.Examples.PingPong as PingPong import Selective.Examples.Call as Call +import Selective.Examples.Fibonacci as Fib +import Selective.Examples.Chat as Chat +import Selective.Examples.Bookstore as Bookstore +import Selective.Examples.TestAC as TestAC + open import Selective.Runtime open import Selective.SimulationEnvironment open import Selective.ActorMonad @@ -9,5 +14,9 @@ open ∞ActorM pingpongEntry = singleton-env (PingPong.spawner .force) callEntry = singleton-env (Call.calltestActor .force) +fibEntry = singleton-env (Fib.spawner .force) +chatEntry = singleton-env (Chat.chat-supervisor .force) +bookstoreEntry = singleton-env (Bookstore.bookstore-supervisor .force) +testacEntry = singleton-env (TestAC.calculator-test-actor .force) -main = IO.run (run-env trace+actors-logger __ENTRY__) +main = IO.run (run-env __ENTRY__) diff --git a/src/Selective/Examples/TestAC.agda b/src/Selective/Examples/TestAC.agda new file mode 100644 index 0000000..f5fa8e0 --- /dev/null +++ b/src/Selective/Examples/TestAC.agda @@ -0,0 +1,92 @@ +module Selective.Examples.TestAC where + +open import Selective.ActorMonad public +open import Selective.Examples.Channel public +open import Selective.Examples.Call2 public +open import Selective.Examples.ActiveObjects public + +open import Data.List using (List ; _∷_ ; [] ; _++_ ; map) +open import Data.List.All using (All ; _∷_ ; []) renaming (map to ∀map) +open import Data.Bool using (Bool ; if_then_else_ ; false ; true) +open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; _*_ ; _≟_ ) +open import Size +open import Level using (Lift ; lift) renaming (zero to lzero ; suc to lsuc) +open import Data.List.Any using (here ; there) +open import Relation.Binary.PropositionalEquality + using (_≡_ ; refl ; cong ; sym ; inspect ; [_] ; trans) +open import Membership using ( + _∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] + ; ⊆-refl ; ⊆-trans ; ⊆-suc ; translate-⊆ + ; lookup-all + ) +open import Data.Unit using (⊤ ; tt) +open import Relation.Nullary using (yes ; no) +open import Relation.Nullary.Decidable using (⌊_⌋) +open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) +open import Level using (Lift ; lift) renaming (zero to lzero ; suc to lsuc) + +open import Debug +open import Data.Nat.Show using (show) + +calculator-ci : ChannelInitiation +calculator-ci = record { + request = Calculator + ; response = record { channel-shape = CalculatorResponse ; all-tagged = (HasTag _) ∷ [] } + ; request-tagged = (HasTag+Ref _) ∷ [] } + +calculator-methods : List ChannelInitiation +calculator-methods = calculator-ci ∷ calculator-ci ∷ [] + +calculator-inbox = active-inbox-shape calculator-methods + +add : (active-method calculator-inbox ⊤₁ (λ _ → []) calculator-ci) +add (Msg Z (n ∷ m ∷ [])) v = return₁ (record { new-state = _ ; reply = SendM Z ((lift (n + m)) ∷ []) }) +add (Msg (S ()) _) _ + +multiply : (active-method calculator-inbox ⊤₁ (λ _ → []) calculator-ci) +multiply (Msg Z (n ∷ m ∷ [])) v = return₁ (record { new-state = _ ; reply = SendM Z ((lift (n * m)) ∷ []) }) +multiply (Msg (S ()) _) _ + +calculator : ActiveObject +calculator = record { + state-type = ⊤₁ + ; vars = λ _ → [] + ; methods = calculator-methods + ; handlers = add ∷ multiply ∷ [] + } + +calculator-actor = run-active-object calculator _ + +calculator-test-actor : ∀{i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → []) +calculator-test-actor = do + spawn∞ calculator-actor + Msg Z (_ ∷ n ∷ []) ← call CalculatorProtocol (record { + var = Z + ; chosen-field = Z + ; fields = (lift 32) ∷ ((lift 10) ∷ []) + ; session = record { + can-request = Z ∷ [] + ; response-session = record { + can-receive = Z ∷ [] + ; tag = 0 + } + } + }) + where + Msg (S ()) _ + Msg Z (_ ∷ m ∷ []) ← debug (show n) (call CalculatorProtocol (record { + var = Z + ; chosen-field = Z + ; fields = (lift 32) ∷ ((lift 10) ∷ []) + ; session = record { + can-request = (S Z) ∷ [] + ; response-session = record { + can-receive = Z ∷ [] + ; tag = 1 + } + } + })) + where + Msg (S ()) _ + debug (show m) (strengthen []) + return m diff --git a/src/Selective/Runtime.agda b/src/Selective/Runtime.agda index afe4f90..5610808 100644 --- a/src/Selective/Runtime.agda +++ b/src/Selective/Runtime.agda @@ -2,8 +2,8 @@ module Selective.Runtime where open import Selective.Simulate open import Selective.SimulationEnvironment -open import Colist using (Colist ; ∞Colist ; [] ; _∷_) open import Data.List using (List ; _∷_ ; [] ; map ; length) +open import Data.List.All using (All ; _∷_ ; []) open import Data.Nat using (ℕ ; zero ; suc) open import Data.Nat.Show using (show) open import Data.String using (String ; _++_) @@ -12,79 +12,58 @@ open import Data.Unit using (⊤ ; tt) open import Coinduction using ( ♯_ ; ♭) open import Size using (∞) import IO -open ∞Colist +open ∞Trace -Logger = (ℕ → EnvStep → IO.IO ⊤) +record BlockedCount : Set₂ where + field + return-count : ℕ + receive-count : ℕ + selective-count : ℕ + +count-blocked : (env : Env) → BlockedCount +count-blocked env = loop (Env.blocked-no-progress env) + where + open BlockedCount + loop : ∀ {store inbs bl} → All (IsBlocked store inbs) bl → BlockedCount + loop [] = record { return-count = 0 ; receive-count = 0 ; selective-count = 0 } + loop (BlockedReturn _ _ ∷ xs) = + let rec = loop xs + in record { return-count = suc (rec .return-count) ; receive-count = rec .receive-count ; selective-count = rec .selective-count } + loop (BlockedReceive _ _ _ ∷ xs) = + let rec = loop xs + in record { return-count = rec .return-count ; receive-count = suc (rec .receive-count) ; selective-count = rec .selective-count } + loop (BlockedSelective _ _ _ _ _ ∷ xs) = + let rec = loop xs + in record { return-count = rec .return-count ; receive-count = rec .receive-count ; selective-count = suc (rec .selective-count) } + +show-env : Env → String +show-env env = + let count = count-blocked env + open BlockedCount + in "There are " ++ show (count .return-count) ++ " finished actors, " ++ show (count .receive-count) ++ " receiving actors, and " ++ show (count .selective-count) ++ " selecting actors" + +show-final-step : ℕ → String +show-final-step n = "Done after " ++ (show n) ++ " steps." -- run-env continously runs the simulation of an environment -- and transforms the steps taken into output to the console. --- The output can be configured by prodiving different loggers. -run-env : Logger → Env → IO.IO ⊤ -run-env logger env = loop 1 ((simulate env) .force) +run-env : Env → IO.IO ⊤ +run-env env = loop 1 ((simulate env) .force) where - loop : ℕ → Colist ∞ EnvStep → IO.IO ⊤ - loop n [] = IO.putStrLn ("Done after " ++ (show n) ++ " steps.") - loop n (x ∷ xs) = ♯ logger n x IO.>> ♯ loop (suc n) (xs .force) - -open EnvStep -open Env - -showNames : List Name → String -showNames [] = "" -showNames (x ∷ []) = show x -showNames (x ∷ x₁ ∷ names) = show x ++ ", " ++ showNames (x₁ ∷ names) - --- Creates a nicely formatted string out of a step-trace from the simulation -show-trace : Trace → String -show-trace (Return name) = show name ++ " returned" -show-trace (Bind name) = "Bind [ " ++ show name ++ " ]" -show-trace (Spawn spawner spawned) = (show spawner) ++ " spawned " ++ (show spawned) -show-trace (Send sender receiver references) = (show sender) ++ " sent a message to " ++ (show receiver) ++ " forwarding [" ++ showNames references ++ "]" -show-trace (Receive name Nothing) = (show name) ++ " received nothing. It was put in the blocked list" -show-trace (Receive name (Value references)) = (show name) ++ " received a message forwarding [" ++ showNames references ++ "]" -show-trace (Receive name Dropped) = (show name) ++ " received something, but had no bind. It was dropped" -show-trace (Selective name Nothing) = (show name) ++ " selective-received nothing. It was put in the blocked list" -show-trace (Selective name (Value references)) = (show name) ++ " selective-received a message forwarding [" ++ showNames references ++ "]" -show-trace (Selective name Dropped) = (show name) ++ " selective-received something, but had no bind. It was dropped" -show-trace (Strengthen name) = (show name) ++ " was strengthened" -show-trace (Self name) = (show name ++ " used self") - --- Output the string of the trace for this step -log-trace : Trace → IO.IO ⊤ -log-trace trace = IO.putStrLn (show-trace trace ++ ".") - --- Output the number of inboxes in the environment. -log-inbox-count : ∀ {store} → Inboxes store → IO.IO ⊤ -log-inbox-count {store} inboxes = IO.putStrLn ("There are " ++ (show (Data.List.length store)) ++ " inboxes.") - --- Output the number of messages in an inbox -log-message-counts : ∀ {store} → Inboxes store → IO.IO ⊤ -log-message-counts [] = IO.return _ -log-message-counts {inbox# name [ _ ] ∷ store} (x ∷ xs) = ♯ IO.putStrLn ("Inbox #" ++ show name ++ " has " ++ (show (Data.List.length x)) ++ " messages.") IO.>> ♯ log-message-counts xs + loop : ℕ → Trace ∞ → IO.IO ⊤ + loop n (TraceStop env _) = ♯ IO.putStrLn (show-final-step n) IO.>> ♯ IO.putStrLn (show-env env) + loop n (x ∷ xs) = ♯ IO.putStrLn ("Step " ++ show n ) IO.>> ♯ loop (suc n) (xs .force) --- Output the nunmber of inboxes and how many messages are in each inbox. -log-inboxes : ∀ {store} → Inboxes store → IO.IO ⊤ -log-inboxes inboxes = ♯ log-inbox-count inboxes IO.>> ♯ log-message-counts inboxes - --- Output how many actors are currently running and how many actors are blocked. -log-actors+blocked : Env → IO.IO ⊤ -log-actors+blocked env = IO.putStrLn ("[A : " ++ show (length (acts env)) ++ " , B : " ++ show (length (blocked env)) ++ "]") - --- Count the number of steps taken -count-logger : Logger -count-logger n step = IO.putStrLn ((show n)) - -trace-logger : Logger -trace-logger n step = log-trace (trace step) - -trace+inbox-logger : Logger -trace+inbox-logger n step = ♯ trace-logger n step IO.>> ♯ log-inboxes (env-inboxes (env step)) - -count+trace+inbox-logger : Logger -count+trace+inbox-logger n step = ♯ count-logger n step IO.>> ♯ trace+inbox-logger n step - -actors-logger : Logger -actors-logger n step = log-actors+blocked (env step) +run-env-silent : Env → IO.IO ⊤ +run-env-silent env = loop 1 ((simulate env) .force) + where + loop : ℕ → Trace ∞ → IO.IO ⊤ + loop n (TraceStop env _) = IO.putStrLn (show-final-step n) + loop n (x ∷ xs) = ♯ IO.return tt IO.>> ♯ loop (suc n) (xs .force) -trace+actors-logger : Logger -trace+actors-logger n step = ♯ trace-logger n step IO.>> ♯ actors-logger n step +run-env-end : Env → IO.IO Env +run-env-end env = loop ((simulate env) .force) + where + loop : Trace ∞ → IO.IO Env + loop (TraceStop env _) = IO.return env + loop (x ∷ xs) = ♯ IO.return x IO.>> ♯ loop (xs .force) diff --git a/src/Selective/Simulate.agda b/src/Selective/Simulate.agda index 2c5764b..a8e95f9 100644 --- a/src/Selective/Simulate.agda +++ b/src/Selective/Simulate.agda @@ -1,258 +1,358 @@ -module Selective.Simulate where - -open import Membership using (_∈_ ; _⊆_ ; All-⊆ ; translate-⊆ ; ⊆-refl) -open import Selective.ActorMonad public -open import Selective.SimulationEnvironment -open import Selective.EnvironmentOperations -open import Colist - -open import Data.List using (List ; _∷_ ; [] ; map ; _++_) -open import Data.List.All using (All ; _∷_ ; [] ; lookup) renaming (map to ∀map) -open import Data.List.All.Properties using (++⁺) -open import Data.Nat using (ℕ ; zero ; suc ; _≟_ ; _<_ ; s≤s) -open import Data.Nat.Properties using (≤-reflexive ; ≤-step) -open import Data.Unit using (⊤ ; tt) -open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) - -open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; cong ; trans) - -open import Level using (Lift ; lift) renaming (suc to lsuc ; zero to lzero) -open import Size using (∞) - -data ReceiveKind : Set where - Nothing : ReceiveKind - Value : List Name → ReceiveKind - Dropped : ReceiveKind - -data Trace : Set where - Return : Name → Trace - Bind : Name → Trace - Spawn : (spawner : Name) → (spawned : Name) → Trace - Send : (sender : Name) → (receiver : Name) → (references : List Name) → Trace - Receive : Name → ReceiveKind → Trace - Selective : Name → ReceiveKind → Trace - Strengthen : Name → Trace - Self : Name → Trace - --- A step in the simulation is the next environment paired up with what step was taken -record EnvStep : Set₂ where - field - env : Env - trace : Trace - -private - keep-simulating : Trace → Env → ∞Colist ∞ EnvStep - -open Actor -open ValidActor -open Env -open FoundReference -open LiftedReferences -open UpdatedInboxes -open ValidMessageList -open NamedInbox -open _comp↦_∈_ -open ∞Colist -open NameSupply -open NameSupplyStream - --- Simulates the actors running in parallel by making one step of one actor at a time. --- The actor that was run is put in the back of the queue unless it became blocked. --- A simulation can possibly be infinite, and is thus modelled as an infinite list. --- --- The simulation function is structured by pattern matching on every constructor of ActorM --- for the top-most actor. -simulate : Env → ∞Colist ∞ EnvStep -simulate env with (acts env) | (actors-valid env) -simulate env | [] | _ = delay [] -simulate env | actor ∷ rest | _ with (computation actor) -simulate env | actor ∷ rest | _ | Return val ⟶ [] = keep-simulating (Return (name actor)) (drop-top-actor env) -simulate env | actor ∷ rest | valid ∷ restValid | Return val ⟶ (f ∷ cont) = keep-simulating (Return (name actor)) env' - where - actor' : Actor - actor' = replace-actorM actor ((f val) .force ⟶ cont) - env' : Env - env' = replace-actors - env - (actor' ∷ rest) - (rewrap-valid-actor valid refl refl refl ∷ restValid) -simulate env | actor ∷ rest | valid ∷ restValid | (m ∞>>= f) ⟶ cont = keep-simulating (Bind (name actor)) env' - where - actor' : Actor - actor' = replace-actorM actor (m .force ⟶ (f ∷ cont)) - env' : Env - env' = replace-actors - env - (actor' ∷ rest) - (rewrap-valid-actor valid refl refl refl ∷ restValid) -simulate env | actor ∷ rest | valid ∷ restValid | Spawn {NewIS} {B} act ⟶ cont = keep-simulating (Spawn (name actor) (env .name-supply .supply .name)) env' - where - newStoreEntry : NamedInbox - newStoreEntry = inbox# (env .name-supply .supply .name) [ NewIS ] - newStore : Store - newStore = newStoreEntry ∷ store env - newAct : Actor - newAct = new-actor act (env .name-supply .supply .name) - newActValid : ValidActor newStore newAct - newActValid = record { actor-has-inbox = zero ; references-have-pointer = [] } - actor' : Actor - actor' = add-reference actor newStoreEntry (Return _ ⟶ cont) - valid' : ValidActor newStore actor' - valid' = record { - actor-has-inbox = suc {pr = env .name-supply .supply .name-is-fresh (actor-has-inbox valid)} (actor-has-inbox valid) - ; references-have-pointer = [p: zero ][handles: ⊆-refl ] ∷ ∀map - (λ p → suc-p (env .name-supply .supply .name-is-fresh (actual-has-pointer p)) p) - (references-have-pointer valid) } - env' : Env - env' = record - { acts = newAct ∷ actor' ∷ rest - ; blocked = blocked env - ; store = newStore - ; env-inboxes = [] ∷ env-inboxes env - ; actors-valid = newActValid ∷ valid' ∷ ∀map (valid-actor-suc (env .name-supply .supply)) restValid - ; blocked-valid = ∀map (valid-actor-suc (env .name-supply .supply)) (blocked-valid env) - ; messages-valid = [] ∷ map-suc (store env) (messages-valid env) (env .name-supply .supply) - ; name-supply = env .name-supply .next NewIS - } - where - map-suc : (store : Store) → {store' : Store} {inbs : Inboxes store'} → InboxesValid store inbs → (ns : NameSupply store) → InboxesValid (inbox# ns .name [ NewIS ] ∷ store) inbs - map-suc store [] ns = [] - map-suc store (x ∷ valid) ns = messages-valid-suc ns x ∷ map-suc store valid ns -simulate env | actor ∷ rest | valid ∷ restValid | Send {ToIS = ToIS} canSendTo (SendM tag fields) ⟶ cont = - keep-simulating (Send (name actor) (name foundTo) (reference-names namedFields)) withUnblocked - where - foundTo : FoundReference (store env) ToIS - foundTo = lookup-reference-act valid canSendTo - namedFields = name-fields-act (store env) actor fields valid - actor' : Actor - actor' = replace-actorM actor (Return _ ⟶ cont) - withM : Env - withM = replace-actors - env - (actor' ∷ rest) - ((rewrap-valid-actor valid refl refl refl) ∷ restValid) - withUpdatedInbox : Env - withUpdatedInbox = update-inbox-env - withM - (underlying-pointer foundTo) - (add-message - (NamedM - (translate-message-pointer foundTo tag) - namedFields) - (make-pointers-compatible - (store env) - (pre actor) - (references actor) - (pre-eq-refs actor) - fields - (references-have-pointer valid))) - withUnblocked : Env - withUnblocked = unblock-actor withUpdatedInbox (name foundTo) -simulate env | actor ∷ rest | valid ∷ restValid | Receive ⟶ cont = keep-simulating (Receive (name actor) (receiveKind (GetInbox.messages actorsInbox))) (env' actorsInbox) - where - actorsInbox : GetInbox (store env) (inbox-shape actor) - actorsInbox = get-inbox env (actor-has-inbox valid) - inboxesAfter = update-inboxes (store env) (env-inboxes env) (messages-valid env) (actor-has-inbox valid) remove-message - receiveKind : List (NamedMessage (inbox-shape actor)) → ReceiveKind - receiveKind [] = Nothing - receiveKind (NamedM _ ps ∷ xs) = Value (reference-names ps) - env' : GetInbox (store env) (inbox-shape actor) → Env - env' record { messages = [] } = replace-actors+blocked - env - rest - restValid - (actor ∷ blocked env) - (valid ∷ blocked-valid env) - env' record { messages = (nm ∷ messages) ; valid = nmv ∷ vms } = record - { acts = add-references-rewrite - actor - (named-inboxes nm) - {unname-message nm} - (add-references++ - nm - nmv - (pre actor)) - (Return (unname-message nm) ⟶ cont) - ∷ rest - ; blocked = blocked env - ; store = store env - ; env-inboxes = updated-inboxes inboxesAfter - ; actors-valid = record { - actor-has-inbox = actor-has-inbox valid - ; references-have-pointer = valid++ - nm - nmv - (references-have-pointer valid) } - ∷ restValid - ; blocked-valid = blocked-valid env - ; messages-valid = inboxes-valid inboxesAfter - ; name-supply = env .name-supply - } -simulate env | actor ∷ rest | valid ∷ restValid | SelectiveReceive filter ⟶ cont = keep-simulating (Selective (name actor) (receiveKind selectedMessage)) (env' selectedMessage) - where - actorsInbox : GetInbox (store env) (inbox-shape actor) - actorsInbox = get-inbox env (actor-has-inbox valid) - selectedMessage : FoundInList (GetInbox.messages actorsInbox) (λ x → filter (unname-message x)) - selectedMessage = find-split (GetInbox.messages actorsInbox) (λ x → filter (unname-message x)) - inboxesAfter = update-inboxes (store env) (env-inboxes env) - (messages-valid env) (actor-has-inbox valid) - (remove-found-message filter) - receiveKind : FoundInList (GetInbox.messages actorsInbox) (λ x → filter (unname-message x)) → ReceiveKind - receiveKind (Found split x) = Value (reference-names (Σ.proj₂ (named-message-fields (el split)))) - where open SplitList - receiveKind Nothing = Nothing - env' : FoundInList (GetInbox.messages actorsInbox) (λ x → filter (unname-message x)) → Env - env' Nothing = replace-actors+blocked env - rest restValid - (actor ∷ blocked env) (valid ∷ blocked-valid env) - env' (Found split x) = record - { acts = add-references-rewrite actor (named-inboxes (SplitList.el split)) - {unname-message (SplitList.el split)} - (add-references++ (SplitList.el split) - (split-all-el - (GetInbox.messages actorsInbox) - (GetInbox.valid actorsInbox) - split) - (pre actor)) - (Return (record { msg = unname-message (SplitList.el split) ; msg-ok = x }) ⟶ cont) ∷ rest - ; blocked = blocked env - ; store = store env - ; env-inboxes = updated-inboxes inboxesAfter - ; actors-valid = (record { - actor-has-inbox = actor-has-inbox valid - ; references-have-pointer = valid++ (SplitList.el split) - (split-all-el (GetInbox.messages actorsInbox) - (GetInbox.valid actorsInbox) - split) - (references-have-pointer valid) - }) ∷ restValid - ; blocked-valid = blocked-valid env - ; messages-valid = inboxes-valid inboxesAfter - ; name-supply = env .name-supply - } -simulate env | actor ∷ rest | valid ∷ restValid | Self ⟶ cont = keep-simulating (Self (name actor)) env' - where - actor' : Actor - actor' = add-reference actor inbox# (name actor) [ (inbox-shape actor) ] (Return _ ⟶ cont) - valid' : ValidActor (store env) actor' - valid' = record { - actor-has-inbox = actor-has-inbox valid - ; references-have-pointer = [p: (actor-has-inbox valid) ][handles: ⊆-refl ] ∷ references-have-pointer valid } - env' : Env - env' = replace-actors env (actor' ∷ rest) (valid' ∷ restValid) -simulate env | actor ∷ rest | valid ∷ restValid | Strengthen {ys} inc ⟶ cont = keep-simulating (Strengthen (name actor)) env' - where - liftedRefs = lift-references inc (references actor) (pre-eq-refs actor) - strengthenedM : ActorM ∞ (inbox-shape actor) ⊤₁ (map shape (contained liftedRefs)) (λ _ → ys) - strengthenedM rewrite (sym (contained-eq-inboxes liftedRefs))= Return _ - actor' : Actor - actor' = lift-actor actor (contained liftedRefs) refl (strengthenedM ⟶ cont) - valid' : ValidActor (store env) actor' - valid' = record { - actor-has-inbox = actor-has-inbox valid - ; references-have-pointer = All-⊆ (subset liftedRefs) (references-have-pointer valid) } - env' : Env - env' = replace-actors env (actor' ∷ rest) (valid' ∷ restValid) - - -keep-simulating trace env .force = record { env = env ; trace = trace } ∷ simulate (top-actor-to-back env) +module Selective.Simulate where + +open import Membership using (_∈_ ; _⊆_ ; All-⊆ ; translate-⊆ ; ⊆-refl) +open import Selective.ActorMonad public +open import Selective.SimulationEnvironment +open import Selective.EnvironmentOperations + +open import Data.List using (List ; _∷_ ; [] ; map ; _++_) +open import Data.List.All using (All ; _∷_ ; [] ; lookup) renaming (map to ∀map) +open import Data.List.All.Properties using (++⁺) +open import Data.Nat using (ℕ ; zero ; suc ; _≟_ ; _<_ ; s≤s) +open import Data.Nat.Properties using (≤-reflexive ; ≤-step) +open import Data.Unit using (⊤ ; tt) +open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) +open import Data.Bool using (Bool ; true ; false) + +open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; cong ; trans ; inspect ; [_]) + +open import Level using (Lift ; lift) renaming (suc to lsuc ; zero to lzero) +open import Size using (∞ ; Size ; Size<_) + +open Actor +open ValidActor +open Env +open FoundReference +open LiftedReferences +open UpdatedInbox +open ValidMessageList +open NamedInbox +open _comp↦_∈_ +open NameSupply +open NameSupplyStream + +data Trace (i : Size) : Set₂ + +record ∞Trace (i : Size) : Set₂ where + coinductive + constructor delay_ + field force : {j : Size< i} → Trace j + +data Trace (i : Size) where + TraceStop : (env : Env) → Done env → Trace i + _∷_ : (x : Env) (xs : ∞Trace i) → Trace i + +reduce-unbound-return : {act : Actor} → (env : Env) → Focus act env → + ActorAtConstructor Return act → + ActorHasNoContinuation act → + Env +reduce-unbound-return env Focused AtReturn no-cont = block-focused env Focused (BlockedReturn AtReturn no-cont) + +reduce-bound-return : {act : Actor} → (env : Env) → Focus act env → + ActorAtConstructor Return act → + ActorHasContinuation act → + Env +reduce-bound-return env@record { + acts = actor@record { computation = Return v ⟶ (f ∷ cont) } ∷ rest + ; actors-valid = actor-valid ∷ rest-valid + } Focused AtReturn HasContinuation = + let + actor' : Actor + actor' = replace-actorM actor ((f v .force) ⟶ cont) + env' : Env + env' = replace-focused + env + Focused + actor' + (rewrap-valid-actor AreSame actor-valid) + in env' + +reduce-bind : {act : Actor} → (env : Env) → Focus act env → + ActorAtConstructor Bind act → + Env +reduce-bind env@record { acts = actor@record { computation = (m ∞>>= f) ⟶ cont } ∷ rest ; actors-valid = actor-valid ∷ rest-valid } Focused AtBind = + let + actor' : Actor + actor' = replace-actorM actor ((m .force) ⟶ (f ∷ cont)) + env' : Env + env' = replace-focused + env + Focused + actor' + (rewrap-valid-actor AreSame actor-valid) + in env' + +reduce-spawn : {act : Actor} → (env : Env) → Focus act env → + ActorAtConstructor Spawn act → + Env +reduce-spawn env@record { + acts = actor@record { computation = Spawn {NewIS} {B} act ⟶ cont } ∷ rest + ; actors-valid = actor-valid ∷ rest-valid + } Focused AtSpawn = + let + new-name : Name + new-name = env .name-supply .supply .name + new-store-entry : NamedInbox + new-store-entry = inbox# new-name [ NewIS ] + env' : Env + env' = add-top (act ⟶ []) env + valid' : ValidActor (env' .store) actor + valid' = valid-actor-suc (env .name-supply .supply) actor-valid + env'' : Env + env'' = top-actor-to-back env' + actor' : Actor + actor' = add-reference actor new-store-entry (Return _ ⟶ cont) + valid'' : ValidActor (env'' .store) actor' + valid'' = add-reference-valid RefAdded valid' [p: zero ][handles: ⊆-refl ] + env''' : Env + env''' = replace-focused env'' Focused actor' valid'' + in env''' + +reduce-send : {act : Actor} → (env : Env) → Focus act env → + ActorAtConstructor Send act → + Env +reduce-send env@record { + acts = actor@record { computation = Send {ToIS = ToIS} canSendTo (SendM tag fields) ⟶ cont } ∷ rest + ; actors-valid = actor-valid ∷ rest-valid + } Focused AtSend = + let + to-reference : FoundReference (store env) ToIS + to-reference = lookup-reference-act actor-valid canSendTo + namedFields = name-fields-act (store env) actor fields actor-valid + actor' : Actor + actor' = replace-actorM actor (Return _ ⟶ cont) + withM : Env + withM = replace-focused + env + Focused + actor' + (rewrap-valid-actor AreSame actor-valid) + message = NamedM + (translate-message-pointer to-reference tag) + namedFields + message-is-valid : message-valid (env .store) message + message-is-valid = make-pointers-compatible + (env .store) + (actor .pre) + (actor .references) + (actor .pre-eq-refs) + fields + (actor-valid .references-have-pointer) + updater = add-message message message-is-valid + withUpdatedInbox : Env + withUpdatedInbox = update-inbox-env + withM + (underlying-pointer to-reference) + updater + in withUpdatedInbox + + +reduce-receive-without-message : {act : Actor} → (env : Env) → Focus act env → + ActorAtConstructor Receive act → + (p : has-inbox (env .store) act) → + inbox-for-actor (env .env-inboxes) act p [] → + Env +reduce-receive-without-message env Focused AtReceive p ifa = block-focused env Focused (BlockedReceive AtReceive p ifa) + +reduce-receive-with-message : {act : Actor} → (env : Env) → Focus act env → + ActorAtConstructor Receive act → + (p : has-inbox (env .store) act) → + ∀ inbox → + all-messages-valid (env .store) inbox → + InboxInState NonEmpty inbox → + inbox-for-actor (env .env-inboxes) act p inbox → + Env +reduce-receive-with-message env@record { + acts = actor@record { computation = (Receive ⟶ cont) } ∷ rest + ; actors-valid = actor-valid ∷ rest-valid + } Focused AtReceive p (nm ∷ messages) (nmv ∷ vms) HasMessage ifa = + let + inboxesAfter = update-inbox + (env .store) + (env .env-inboxes) + (env .messages-valid) + (actor-valid .actor-has-inbox) + remove-message + actor' : Actor + actor' = add-references-rewrite + actor + (named-inboxes nm) + {unname-message nm} + (add-references++ + nm + nmv + (pre actor)) + (Return (unname-message nm) ⟶ cont) + actor-valid' : ValidActor (env .store) actor' + actor-valid' = record { + actor-has-inbox = actor-valid .actor-has-inbox + ; references-have-pointer = valid++ nm nmv (actor-valid .references-have-pointer) + } + env' : Env + env' = let + updated = update-inbox (env .store) (env .env-inboxes) (env .messages-valid) (actor-valid .actor-has-inbox) remove-message + unblock-split = unblock-actors updated (env .blocked) (env .blocked-valid) (env .blocked-no-progress) + open UnblockedActors + in record + { acts = actor' ∷ unblock-split .unblocked ++ rest + ; blocked = unblock-split .still-blocked + ; store = env .store + ; env-inboxes = updated .updated-inboxes + ; name-supply = env .name-supply + ; actors-valid = actor-valid' ∷ ++⁺ (unblock-split .unblocked-valid) rest-valid + ; blocked-valid = unblock-split .blocked-valid + ; messages-valid = updated .inboxes-valid + ; blocked-no-progress = unblock-split .blocked-no-prog + } + in env' + + +reduce-receive : {act : Actor} → (env : Env) → Focus act env → + ActorAtConstructor Receive act → + Env +reduce-receive env@record { acts = actor ∷ rest ; actors-valid = actor-valid ∷ _ } Focused AtReceive = choose-reduction (get-inbox env (actor-valid .actor-has-inbox)) + where + open GetInbox + choose-reduction : (gi : GetInbox (env .store) (env .env-inboxes) (actor-valid .actor-has-inbox)) → Env + choose-reduction gi@record { messages = [] } = + reduce-receive-without-message env Focused AtReceive _ (gi .right-inbox) + choose-reduction gi@record { messages = _ ∷ _ } = + reduce-receive-with-message env Focused AtReceive _ (gi .messages) (gi .valid) HasMessage (gi .right-inbox) + +reduce-self : {act : Actor} → (env : Env) → Focus act env → + ActorAtConstructor Self act → + Env +reduce-self env@record { acts = actor@record { + computation = Self ⟶ cont } ∷ _ + ; actors-valid = actor-valid ∷ _ + } Focused AtSelf = + let + actor' : Actor + actor' = add-reference actor inbox# (actor .name) [ (actor .inbox-shape) ] ((Return _) ⟶ cont) + actor-valid' : ValidActor (env .store) actor' + actor-valid' = add-reference-valid RefAdded actor-valid [p: (actor-valid .actor-has-inbox) ][handles: ⊆-refl ] + env' : Env + env' = replace-focused + env + Focused + actor' + actor-valid' + in env' + +reduce-selective-with-message : {act : Actor} → (env : Env) → Focus act env → + (aac : ActorAtConstructor Selective act) → + (point : has-inbox (env .store) act) → + ∀ inbox → + all-messages-valid (env .store) inbox → + inbox-for-actor (env .env-inboxes) act point inbox → + {split : SplitList inbox} → + {p : (filter-named (selected-filter act aac)) (SplitList.el split) ≡ true} → + InboxInFilterState {filter = filter-named (selected-filter act aac)} inbox (Found split p) → + Env +reduce-selective-with-message env@record { + acts = actor@record { computation = SelectiveReceive filter ⟶ cont } ∷ rest + ; actors-valid = actor-valid ∷ rest-valid + } Focused AtSelective point inb amv ifa (HasMessage {split = split} {ok}) = + let updated = update-inbox (env .store) (env .env-inboxes) (env .messages-valid) (actor-valid .actor-has-inbox) (remove-found-message filter) + unblock-split = unblock-actors updated (env .blocked) (env .blocked-valid) (env .blocked-no-progress) + received-nm = SplitList.el split + added-references = named-inboxes received-nm + received-message = unname-message received-nm + received-valid : message-valid (env .store) received-nm + received-valid = split-all-el inb amv split + adds-correct-references : map shape added-references ++ (actor .pre) ≡ add-references (actor .pre) received-message + adds-correct-references = add-references++ received-nm received-valid (actor .pre) + new-continuation = Return (record { msg = received-message ; msg-ok = ok }) ⟶ cont + act' : Actor + act' = add-references-rewrite actor added-references {received-message} adds-correct-references new-continuation + act-valid' : ValidActor (env .store) act' + act-valid' = record { + actor-has-inbox = actor-valid .actor-has-inbox + ; references-have-pointer = valid++ received-nm received-valid (actor-valid .references-have-pointer) + } + open UnblockedActors + in record + { acts = act' ∷ unblock-split .unblocked ++ rest + ; blocked = unblock-split .still-blocked + ; store = env .store + ; env-inboxes = updated-inboxes updated + ; name-supply = env .name-supply + ; actors-valid = act-valid' ∷ ++⁺ (unblock-split .unblocked-valid) rest-valid + ; blocked-valid = unblock-split .blocked-valid + ; messages-valid = inboxes-valid updated + ; blocked-no-progress = unblock-split .blocked-no-prog + } + +reduce-selective-without-message : {act : Actor} → (env : Env) → Focus act env → + (aac : ActorAtConstructor Selective act) → + (point : has-inbox (env .store) act) → + ∀ inbox → + inbox-for-actor (env .env-inboxes) act point inbox → + InboxInFilterState {filter = filter-named (selected-filter act aac)} inbox Nothing → + Env +reduce-selective-without-message env Focused AtSelective point inbox ifa iifs = + block-focused env Focused (BlockedSelective AtSelective point inbox ifa iifs) + +reduce-selective : {act : Actor} → (env : Env) → Focus act env → + ActorAtConstructor Selective act → + Env +reduce-selective env@record { + acts = actor@record { computation = SelectiveReceive filter ⟶ _ } ∷ _ + ; actors-valid = actor-valid ∷ _ + } Focused AtSelective = + let inb = get-inbox env (actor-valid .actor-has-inbox) + in choose-reduction inb (find-split (inb .messages) (filter-named filter)) + where + open GetInbox + choose-reduction : (gi : GetInbox (env .store) (env .env-inboxes) (actor-valid .actor-has-inbox)) → FoundInList (gi .messages) (filter-named filter) → Env + choose-reduction gi (Found split x) = reduce-selective-with-message env Focused AtSelective _ (gi .messages) (gi .valid) (gi .right-inbox) (HasMessage {split = split} {x}) + choose-reduction gi Nothing = reduce-selective-without-message env Focused AtSelective _ (gi .messages) (gi .right-inbox) IsEmpty + +reduce-strengthen : {act : Actor} → (env : Env) → Focus act env → + ActorAtConstructor Strengthen act → + Env +reduce-strengthen env@record { + acts = actor@record { computation = Strengthen {ys} inc ⟶ cont } ∷ _ + ; actors-valid = actor-valid ∷ _ + } Focused AtStrengthen = + let + lifted-references = lift-references inc (references actor) (pre-eq-refs actor) + actor' : Actor + actor' = lift-actor actor (lifted-references .contained) (lifted-references .contained-eq-inboxes) (Return _ ⟶ cont) + actor-valid' : ValidActor (env .store) actor' + actor-valid' = lift-valid-actor (CanBeLifted lifted-references) actor-valid + env' : Env + env' = replace-focused + env + Focused + actor' + actor-valid' + in env' + +reduce : {act : Actor} → (env : Env) → Focus act env → Env +reduce env@record { acts = record { computation = (Return val ⟶ []) } ∷ _ } Focused = + reduce-unbound-return env Focused AtReturn (NoContinuation {v = val}) +reduce env@record { acts = record { computation = (Return val ⟶ (_ ∷ _)) } ∷ _ } Focused = + reduce-bound-return env Focused AtReturn (HasContinuation {v = val}) +reduce env@record { acts = record { computation = ((m ∞>>= f) ⟶ _)} ∷ _ } Focused = + reduce-bind env Focused AtBind +reduce env@record { acts = record { computation = (Spawn act ⟶ cont) } ∷ _ } Focused = + reduce-spawn env Focused AtSpawn +reduce env@record { acts = record { computation = (Send canSendTo msg ⟶ cont) } ∷ _ } Focused = + reduce-send env Focused AtSend +reduce env@record { acts = record { computation = (Receive ⟶ cont) } ∷ _ } Focused = + reduce-receive env Focused AtReceive +reduce env@record { acts = record { computation = (SelectiveReceive filter ⟶ cont) } ∷ _ } Focused = + reduce-selective env Focused AtSelective +reduce env@record { acts = record { computation = (Self ⟶ cont) } ∷ _ } Focused = + reduce-self env Focused AtSelf +reduce env@record { acts = record { computation = (Strengthen inc ⟶ cont) } ∷ _ } Focused = + reduce-strengthen env Focused AtStrengthen + +simulate : Env → ∞Trace ∞ +simulate env@record { acts = [] ; actors-valid = [] } = delay TraceStop env AllBlocked +simulate env@record { acts = _ ∷ _ ; actors-valid = _ ∷ _ } = keep-stepping (reduce env Focused) + where + open ∞Trace + keep-stepping : Env → ∞Trace ∞ + keep-stepping env .force = env ∷ simulate env diff --git a/src/Selective/SimulationEnvironment.agda b/src/Selective/SimulationEnvironment.agda index 5a8d1e7..f0c257a 100644 --- a/src/Selective/SimulationEnvironment.agda +++ b/src/Selective/SimulationEnvironment.agda @@ -1,20 +1,22 @@ module Selective.SimulationEnvironment where -open import Membership using (_∈_ ; find-∈) +open import Membership using (_∈_ ; find-∈ ; _⊆_) open import Selective.ActorMonad +open import NatProps -open import Data.List using (List ; _∷_ ; [] ; map) +open import Data.List using (List ; _∷_ ; [] ; map ; _++_ ; drop) open import Data.List.All using (All ; _∷_ ; [] ; lookup) renaming (map to ∀map) open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) open import Data.Nat using (ℕ ; _≟_ ; _<_ ; zero ; suc ; s≤s) open import Data.Nat.Properties using (≤-reflexive ; ≤-step) open import Data.Unit using (⊤ ; tt) +open import Data.Bool using (Bool ; true ; false) -open import Level using (Lift ; lift) +open import Level using (Level ; Lift ; lift) renaming (suc to lsuc) open import Size using (Size ; Size<_ ; ↑_ ; ∞) open import Data.Empty using (⊥) open import Relation.Nullary using (Dec ; yes ; no ; ¬_) -open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym) +open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; cong ; cong₂ ; trans ; inspect ; [_]) open import Relation.Unary using (Decidable) renaming (_⊆_ to _⋐_) -- We give every actor and inbox a name. @@ -48,15 +50,6 @@ record NamedInbox : Set₁ where -- Inserting duplicate keys is thus pointless and is not done anywhere in the code. Store = List NamedInbox --- Decidable inequality -¬[_] : ∀ {a b : Name} → Dec (a ≡ b) → Set -¬[ (yes x₁) ] = ⊥ -¬[ (no x₁) ] = ⊤ - --- Also decidable inequality -_¬≡_ : ( a b : Name) → Set -a ¬≡ b = ¬[ a ≟ b ] - -- A pointer into the store. -- This is a proof that the name points to an inbox shape in the store. -- The store is a key-value list that returns the first value matching the key (name). @@ -66,7 +59,7 @@ a ¬≡ b = ¬[ a ≟ b ] data _↦_∈e_ (n : Name) (S : InboxShape) : Store → Set where zero : ∀ {xs} → n ↦ S ∈e (inbox# n [ S ] ∷ xs) - suc : ∀ {n' : Name} { S' xs} {pr : n ¬≡ n'} + suc : ∀ {n' : Name} { S' xs} {pr : ¬ n ≡ n'} → n ↦ S ∈e xs → n ↦ S ∈e (inbox# n' [ S' ] ∷ xs) @@ -129,26 +122,49 @@ named-field-content (ReferenceType Fw) = Name -- The decision to use names for references and pointers, rather than just ∈, -- makes it possible to prove that a sent message containing a reference -- does not need to be modified when more actors are added. -data NamedMessage (To : InboxShape): Set₁ where - NamedM : {MT : MessageType} → MT ∈ To → All named-field-content MT → NamedMessage To +record NamedMessage (To : InboxShape): Set₁ where + constructor NamedM + field + {MT} : MessageType + named-message-type : MT ∈ To + named-fields : All named-field-content MT + +unname-message : ∀ {S} → NamedMessage S → Message S +unname-message (NamedM x fields) = Msg x (do-the-work fields) + where + do-the-work : ∀ {MT} → All named-field-content MT → All receive-field-content MT + do-the-work {[]} nfc = [] + do-the-work {ValueType x₁ ∷ MT} (px ∷ nfc) = px ∷ (do-the-work nfc) + do-the-work {ReferenceType x₁ ∷ MT} (px ∷ nfc) = _ ∷ do-the-work nfc -named-message-fields : ∀ {To} → NamedMessage To → Σ[ MT ∈ MessageType ] All named-field-content MT -named-message-fields (NamedM {MT} x x₁) = MT , x₁ +filter-named : ∀ {IS} → MessageFilter IS → NamedMessage IS → Bool +filter-named filter message = filter (unname-message message) Inbox : InboxShape → Set₁ Inbox is = List (NamedMessage is) data Inboxes : (store : Store) → Set₁ where [] : Inboxes [] - _∷_ : ∀ {store name inbox-shape} → List (NamedMessage inbox-shape) → + _∷_ : ∀ {store name inbox-shape} → Inbox inbox-shape → (inboxes : Inboxes store) → Inboxes (inbox# name [ inbox-shape ] ∷ store) +data InboxForPointer {inbox-shape : InboxShape} (inbox : Inbox inbox-shape) {name : Name} : (store : Store) → (Inboxes store) → (name ↦ inbox-shape ∈e store) → Set₁ where + zero : ∀ {store} {inbs : Inboxes store} → + InboxForPointer inbox (inbox# name [ inbox-shape ] ∷ store) (inbox ∷ inbs) zero + suc : ∀ {n' : Name} {S' inb' store} {p : name ↦ inbox-shape ∈e store} {inbs : Inboxes store} {pr : ¬ name ≡ n'} → + InboxForPointer inbox store inbs p → + InboxForPointer inbox (inbox# n' [ S' ] ∷ store) (inb' ∷ inbs) (suc {pr = pr} p) + -- Property that there exists an inbox of the right shape in the list of inboxes -- This is used both for proving that every actor has an inbox, -- and for proving that every reference known by an actor has an inbox has-inbox : Store → Actor → Set has-inbox store actor = Actor.name actor ↦ Actor.inbox-shape actor ∈e store + +inbox-for-actor : ∀ {store} (inbs : Inboxes store) (actor : Actor) (p : has-inbox store actor) (inb : Inbox (Actor.inbox-shape actor)) → Set₁ +inbox-for-actor {store} inbs actor p inb = InboxForPointer inb store inbs p + reference-has-pointer : Store → NamedInbox → Set₁ reference-has-pointer store ni = name ni comp↦ shape ni ∈ store where open NamedInbox @@ -203,27 +219,16 @@ NameFresh : Store → ℕ → Set₁ NameFresh store n = All (λ v → name v Data.Nat.< n) store where open NamedInbox - --- convert < to ¬≡ -<-¬≡ : ∀ {n m} → n < m → n ¬≡ m -<-¬≡ {zero} {zero} () -<-¬≡ {zero} {suc m} p = _ -<-¬≡ {suc n} {zero} () -<-¬≡ {suc n} {suc m} (Data.Nat.s≤s p) with (<-¬≡ p) -... | q with (n ≟ m) -<-¬≡ {suc n} {suc m} (Data.Nat.s≤s p) | () | yes p₁ -<-¬≡ {suc n} {suc m} (Data.Nat.s≤s p) | q | no ¬p = _ - -- If a name is fresh for a store (i.e. all names in the store are < than the name), -- then none of the names in the store is equal to the name -Fresh¬≡ : ∀ {store name } → NameFresh store name → (All (λ m → (NamedInbox.name m) ¬≡ name) store) +Fresh¬≡ : ∀ {store name } → NameFresh store name → (All (λ m → ¬ (NamedInbox.name m) ≡ name) store) Fresh¬≡ ls = ∀map (λ frsh → <-¬≡ frsh) ls record NameSupply (store : Store) : Set₁ where field name : Name freshness-carrier : All (λ v → NamedInbox.name v < name) store - name-is-fresh : {n : Name} {IS : InboxShape} → n ↦ IS ∈e store → ¬[ n ≟ name ] + name-is-fresh : {n : Name} {IS : InboxShape} → n ↦ IS ∈e store → ¬ n ≡ name open NameSupply @@ -239,11 +244,11 @@ record NameSupplyStream (i : Size) (store : Store) : Set₁ where suc-helper : ∀ {store name IS n} → name ↦ IS ∈e store → All (λ v → suc (NamedInbox.name v) Data.Nat.≤ n) store → - ¬[ name ≟ n ] + ¬ name ≡ n suc-helper zero (px ∷ p) = <-¬≡ px suc-helper (suc q) (px ∷ p) = suc-helper q p -suc-p : ∀ {store name n x shape} → ¬[ name ≟ n ] → name comp↦ shape ∈ store → name comp↦ shape ∈ (inbox# n [ x ] ∷ store) +suc-p : ∀ {store name n x shape} → ¬ name ≡ n → name comp↦ shape ∈ store → name comp↦ shape ∈ (inbox# n [ x ] ∷ store) suc-p pr [p: actual-has-pointer ][handles: actual-handles-wanted ] = [p: (suc {pr = pr} actual-has-pointer) ][handles: actual-handles-wanted ] open NameSupplyStream @@ -269,25 +274,254 @@ name-supply-singleton .next = stream-builder (name-supply-singleton .supply) stream-builder ns IS .supply = next-name-supply ns IS stream-builder ns IS .next = stream-builder (next-name-supply ns IS) +data ActorConstructor : Set where + Return : ActorConstructor + Bind : ActorConstructor + Spawn : ActorConstructor + Send : ActorConstructor + Receive : ActorConstructor + Self : ActorConstructor + Strengthen : ActorConstructor + Selective : ActorConstructor + +data ActorAtConstructor : ActorConstructor → Actor → Set₂ where + AtReturn : + ∀ {IS A B refs mid post name} + {cont : ContStack ∞ IS mid post} + {v : A} + {per} → + ActorAtConstructor Return (record + { inbox-shape = IS + ; A = B + ; references = refs + ; pre = mid v + ; pre-eq-refs = per + ; post = post + ; computation = Return v ⟶ cont + ; name = name + }) + AtBind : + ∀ {IS A B C refs pre mid name} + {m : ∞ActorM ∞ IS A pre mid} + {post : B → TypingContext} + {f : (x : A) → + ∞ActorM ∞ IS B (mid x) post} + {contpost : C → TypingContext} + {cont : ContStack ∞ IS post contpost} → + ∀ {per} → + ActorAtConstructor Bind (record + { inbox-shape = IS + ; A = C + ; references = refs + ; pre = pre + ; pre-eq-refs = per + ; post = contpost + ; computation = (m ∞>>= f) ⟶ cont + ; name = name + }) + AtSpawn : + ∀ {IS NewIS A B refs pre post postN name} + {m : ActorM ∞ NewIS A [] postN} + {cont : ContStack ∞ IS (λ _ → NewIS ∷ pre) post} + {per} → + ActorAtConstructor Spawn (record + { inbox-shape = IS + ; A = B + ; references = refs + ; pre = pre + ; pre-eq-refs = per + ; post = post + ; computation = Spawn m ⟶ cont + ; name = name + }) + AtSend : + ∀ {IS ToIS A refs pre post name} + {canSendTo : pre ⊢ ToIS} + {msg : SendMessage ToIS pre} + {cont : ContStack ∞ IS (λ _ → pre) post} + {per} → + ActorAtConstructor Send (record + { inbox-shape = IS + ; A = A + ; references = refs + ; pre = pre + ; pre-eq-refs = per + ; post = post + ; computation = (Send canSendTo msg) ⟶ cont + ; name = name + }) + AtReceive : + ∀ {IS A refs pre post name} + {cont : ContStack ∞ IS (add-references pre) post} + {per} → + ActorAtConstructor Receive (record + { inbox-shape = IS + ; A = A + ; references = refs + ; pre = pre + ; pre-eq-refs = per + ; post = post + ; computation = Receive ⟶ cont + ; name = name + }) + AtSelective : + ∀ {IS A refs pre post name} + {filter : MessageFilter IS} + {cont : ContStack ∞ IS (add-selected-references pre) post} + {per} → + ActorAtConstructor Selective (record + { inbox-shape = IS + ; A = A + ; references = refs + ; pre = pre + ; pre-eq-refs = per + ; post = post + ; computation = SelectiveReceive filter ⟶ cont + ; name = name + }) + AtSelf : + ∀ {IS A refs pre post name} + {cont : ContStack ∞ IS (λ _ → IS ∷ pre) post} + {per} → + ActorAtConstructor Self (record + { inbox-shape = IS + ; A = A + ; references = refs + ; pre = pre + ; pre-eq-refs = per + ; post = post + ; computation = Self ⟶ cont + ; name = name + }) + AtStrengthen : + ∀ {IS A refs ys xs post name} + {inc : ys ⊆ xs} + {cont : ContStack ∞ IS (λ _ → ys) post} + {per} → + ActorAtConstructor Strengthen (record + { inbox-shape = IS + ; A = A + ; references = refs + ; pre = xs + ; pre-eq-refs = per + ; post = post + ; computation = (Strengthen inc) ⟶ cont + ; name = name + }) + +data ActorHasContinuation : Actor → Set₂ where + HasContinuation : + ∀ {IS A B C refs pre mid contmid post name} + {m : ActorM ∞ IS A pre mid} + {f : Cont ∞ IS {A} {B} mid contmid} + {cont : ContStack ∞ IS contmid post} + {v : A} + {per} → + ActorHasContinuation (record + { inbox-shape = IS + ; A = C + ; references = refs + ; pre = pre + ; pre-eq-refs = per + ; post = post + ; computation = m ⟶ (f ∷ cont) + ; name = name + }) + +data ActorHasNoContinuation : Actor → Set₂ where + NoContinuation : + ∀ {IS A refs pre post name} + {m : ActorM ∞ IS A pre post} + {v : A} + {per} → + ActorHasNoContinuation (record + { inbox-shape = IS + ; A = A + ; references = refs + ; pre = pre + ; pre-eq-refs = per + ; post = post + ; computation = m ⟶ [] + ; name = name + }) + +record SplitList {a : Level} {A : Set a} (ls : List A) : Set (lsuc a) where + field + heads : List A + el : A + tails : List A + is-ls : (heads) ++ (el ∷ tails) ≡ ls + +data FoundInList {a : Level} {A : Set a} (ls : List A) (f : A → Bool) : Set (lsuc a) where + Found : (split : SplitList ls) → (f (SplitList.el split) ≡ true) → FoundInList ls f + Nothing : FoundInList ls f + +find-split : {a : Level} {A : Set a} (ls : List A) (f : A → Bool) → FoundInList ls f +find-split [] f = Nothing +find-split (x ∷ ls) f with (f x) | (inspect f x) +... | false | p = add-x (find-split ls f) + where + add-x : FoundInList ls f → FoundInList (x ∷ ls) f + add-x (Found split x₁) = Found (record { heads = x ∷ heads split ; el = el split ; tails = tails split ; is-ls = cong (_∷_ x) (is-ls split) }) x₁ + where open SplitList + add-x Nothing = Nothing +... | true | [ eq ] = Found (record { heads = [] ; el = x ; tails = ls ; is-ls = refl }) eq + +split-all-el : ∀ {a p} {A : Set a} {P : A → Set p} (ls : List A) → All P ls → (sl : SplitList ls) → (P (SplitList.el sl)) +split-all-el [] ps record { heads = [] ; el = el ; tails = tails ; is-ls = () } +split-all-el [] ps record { heads = (x ∷ heads) ; el = el ; tails = tails ; is-ls = () } +split-all-el (x ∷ ls) (px ∷ ps) record { heads = [] ; el = .x ; tails = .ls ; is-ls = refl } = px +split-all-el (x ∷ ls) (px ∷ ps) record { heads = (x₁ ∷ heads) ; el = el ; tails = tails ; is-ls = refl } = + split-all-el ls ps (record { heads = heads ; el = el ; tails = tails ; is-ls = refl }) + +data InboxState : Set where + Empty NonEmpty : InboxState + +data InboxInState {S : InboxShape} : InboxState → Inbox S → Set₁ where + IsEmpty : InboxInState Empty [] + HasMessage : {nm : NamedMessage S} {rest : Inbox S} → InboxInState NonEmpty (nm ∷ rest) + +data InboxInFilterState {S : InboxShape} {filter : NamedMessage S → Bool} (inbox : Inbox S) : FoundInList inbox filter → Set₁ where + IsEmpty : InboxInFilterState inbox Nothing + HasMessage : {split : SplitList inbox} {p : filter (SplitList.el split) ≡ true} → InboxInFilterState inbox (Found split p) + +selected-filter : ∀ actor → ActorAtConstructor Selective actor → MessageFilter (Actor.inbox-shape actor) +selected-filter record { computation = SelectiveReceive filter ⟶ _ } AtSelective = filter + +data IsBlocked (store : Store) (inbs : Inboxes store) (actor : Actor) : Set₂ where + BlockedReturn : + ActorAtConstructor Return actor → + ActorHasNoContinuation actor → + IsBlocked store inbs actor + BlockedReceive : + ActorAtConstructor Receive actor → + (p : has-inbox store actor) → + InboxForPointer [] store inbs p → + IsBlocked store inbs actor + BlockedSelective : + (aac : ActorAtConstructor Selective actor) → + (point : has-inbox store actor) → + ∀ inbox → + InboxForPointer inbox store inbs point → + InboxInFilterState {filter = filter-named (selected-filter actor aac)} inbox Nothing → + IsBlocked store inbs actor + -- The environment is a list of actors and inboxes, -- with a proof that every ector is valid in the context of said list of inboxes record Env : Set₂ where field - -- The currently active actors + -- raw acts : List Actor - -- The currently blocked actors, i.e. actors doing receive without any messages in its inbox. - -- By separating blocked and non-blocked actors we both optimize the simulation to not try to run - -- actors that won't succed in taking a step, and we get a clear step-condition when there are no - -- non-blocked actors left. blocked : List Actor store : Store env-inboxes : Inboxes store - -- The proofs that an actor and a blocked actor is valid is actually the same proof, - -- but kept in a separate list. + name-supply : NameSupplyStream ∞ store + -- coherence actors-valid : All (ValidActor store) acts blocked-valid : All (ValidActor store) blocked messages-valid : InboxesValid store env-inboxes - name-supply : NameSupplyStream ∞ store + -- weak progress + blocked-no-progress : All (IsBlocked store env-inboxes) blocked -- The empty environment empty-env : Env @@ -300,6 +534,7 @@ empty-env = record ; blocked-valid = [] ; messages-valid = [] ; name-supply = name-supply-singleton + ; blocked-no-progress = [] } -- An environment containing a single actor. @@ -323,4 +558,51 @@ singleton-env {IS} {A} {post} actor = record ; blocked-valid = [] ; messages-valid = [] ∷ [] ; name-supply = name-supply-singleton .next IS + ; blocked-no-progress = [] } + + +data Focus (act : Actor) : Env → Set₂ where + Focused : + {rest : List Actor} + {bl : List Actor} + {str : Store} + {inbs : Inboxes str} + {rv : All (ValidActor str) rest} + {bv : All (ValidActor str) bl} + {bib : All (IsBlocked str inbs) bl} + {mv : InboxesValid str inbs} + {ns : NameSupplyStream ∞ str} + {va : ValidActor str act} → + Focus act (record + { acts = act ∷ rest + ; blocked = bl + ; store = str + ; env-inboxes = inbs + ; actors-valid = va ∷ rv + ; blocked-valid = bv + ; messages-valid = mv + ; name-supply = ns + ; blocked-no-progress = bib + }) + +data Done : Env → Set₂ where + AllBlocked : + {bl : List Actor} + {str : Store} + {inbs : Inboxes str} + {bv : All (ValidActor str) bl} + {bib : All (IsBlocked str inbs) bl} + {mv : InboxesValid str inbs} + {ns : NameSupplyStream ∞ str} → + Done (record + { acts = [] + ; blocked = bl + ; store = str + ; env-inboxes = inbs + ; name-supply = ns + ; actors-valid = [] + ; blocked-valid = bv + ; messages-valid = mv + ; blocked-no-progress = bib + }) diff --git a/src/Simulate.agda b/src/Simulate.agda index d09642f..8448819 100644 --- a/src/Simulate.agda +++ b/src/Simulate.agda @@ -4,7 +4,6 @@ open import Membership using (_∈_ ; _⊆_ ; All-⊆ ; translate-⊆ ; ⊆-refl open import ActorMonad public open import SimulationEnvironment open import EnvironmentOperations -open import Colist open import Data.List using (List ; _∷_ ; [] ; map ; _++_) open import Data.List.All using (All ; _∷_ ; [] ; lookup) renaming (map to ∀map) @@ -14,202 +13,274 @@ open import Data.Nat.Properties using (≤-reflexive ; ≤-step) open import Data.Unit using (⊤ ; tt) open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) -open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; cong ; trans) +open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; cong ; trans ; inspect ; [_]) open import Level using (Lift ; lift) renaming (suc to lsuc ; zero to lzero) -open import Size using (∞) - -data ReceiveKind : Set where - Nothing : ReceiveKind - Value : List Name → ReceiveKind - Dropped : ReceiveKind - -data Trace : Set where - Return : Name → Trace - Bind : Name → Trace - Spawn : (spawner : Name) → (spawned : Name) → Trace - Send : (sender : Name) → (receiver : Name) → (references : List Name) → Trace - Receive : Name → ReceiveKind → Trace - Strengthen : Name → Trace - Self : Name → Trace - --- A step in the simulation is the next environment paired up with what step was taken -record EnvStep : Set₂ where - field - env : Env - trace : Trace - -private - keep-simulating : Trace → Env → ∞Colist ∞ EnvStep +open import Size using (∞ ; Size ; Size<_) open Actor open ValidActor open Env open FoundReference open LiftedReferences -open UpdatedInboxes +open UpdatedInbox open ValidMessageList open NamedInbox open _comp↦_∈_ -open ∞Colist open NameSupply open NameSupplyStream --- Simulates the actors running in parallel by making one step of one actor at a time. --- The actor that was run is put in the back of the queue unless it became blocked. --- A simulation can possibly be infinite, and is thus modelled as an infinite list. --- --- The simulation function is structured by pattern matching on every constructor of ActorM --- for the top-most actor. -simulate : Env → ∞Colist ∞ EnvStep -simulate env with (acts env) | (actors-valid env) -simulate env | [] | _ = delay [] -simulate env | actor ∷ rest | _ with (computation actor) -simulate env | actor ∷ rest | _ | Return val ⟶ [] = keep-simulating (Return (name actor)) (drop-top-actor env) -simulate env | actor ∷ rest | valid ∷ restValid | Return val ⟶ (f ∷ cont) = keep-simulating (Return (name actor)) env' - where +data Trace (i : Size) : Set₂ + +record ∞Trace (i : Size) : Set₂ where + coinductive + constructor delay_ + field force : {j : Size< i} → Trace j + +data Trace (i : Size) where + TraceStop : (env : Env) → Done env → Trace i + _∷_ : (x : Env) (xs : ∞Trace i) → Trace i + +reduce-unbound-return : {act : Actor} → (env : Env) → Focus act env → + ActorAtConstructor Return act → + ActorHasNoContinuation act → + Env +reduce-unbound-return env Focused AtReturn no-cont = block-focused env Focused (BlockedReturn AtReturn no-cont) + +reduce-bound-return : {act : Actor} → (env : Env) → Focus act env → + ActorAtConstructor Return act → + ActorHasContinuation act → + Env +reduce-bound-return env@record { + acts = actor@record { computation = Return v ⟶ (f ∷ cont) } ∷ rest + ; actors-valid = actor-valid ∷ rest-valid + } Focused AtReturn HasContinuation = + let + actor' : Actor + actor' = replace-actorM actor ((f v .force) ⟶ cont) + env' : Env + env' = replace-focused + env + Focused + actor' + (rewrap-valid-actor AreSame actor-valid) + in env' + +reduce-bind : {act : Actor} → (env : Env) → Focus act env → + ActorAtConstructor Bind act → + Env +reduce-bind env@record { acts = actor@record { computation = (m ∞>>= f) ⟶ cont } ∷ rest ; actors-valid = actor-valid ∷ rest-valid } Focused AtBind = + let actor' : Actor - actor' = replace-actorM actor ((f val) .force ⟶ cont) + actor' = replace-actorM actor ((m .force) ⟶ (f ∷ cont)) env' : Env - env' = replace-actors + env' = replace-focused env - (actor' ∷ rest) - (rewrap-valid-actor valid refl refl refl ∷ restValid) -simulate env | actor ∷ rest | valid ∷ restValid | (m ∞>>= f) ⟶ cont = keep-simulating (Bind (name actor)) env' - where - actor' : Actor - actor' = replace-actorM actor (m .force ⟶ (f ∷ cont)) + Focused + actor' + (rewrap-valid-actor AreSame actor-valid) + in env' + +reduce-spawn : {act : Actor} → (env : Env) → Focus act env → + ActorAtConstructor Spawn act → + Env +reduce-spawn env@record { + acts = actor@record { computation = Spawn {NewIS} {B} act ⟶ cont } ∷ rest + ; actors-valid = actor-valid ∷ rest-valid + } Focused AtSpawn = + let + new-name : Name + new-name = env .name-supply .supply .name + new-store-entry : NamedInbox + new-store-entry = inbox# new-name [ NewIS ] env' : Env - env' = replace-actors - env - (actor' ∷ rest) - (rewrap-valid-actor valid refl refl refl ∷ restValid) -simulate env | actor ∷ rest | valid ∷ restValid | Spawn {NewIS} {B} act ⟶ cont = keep-simulating (Spawn (name actor) (env .name-supply .supply .name)) env' - where - newStoreEntry : NamedInbox - newStoreEntry = inbox# (env .name-supply .supply .name) [ NewIS ] - newStore : Store - newStore = newStoreEntry ∷ store env - newAct : Actor - newAct = new-actor act (env .name-supply .supply .name) - newActValid : ValidActor newStore newAct - newActValid = record { actor-has-inbox = zero ; references-have-pointer = [] } + env' = add-top (act ⟶ []) env + valid' : ValidActor (env' .store) actor + valid' = valid-actor-suc (env .name-supply .supply) actor-valid + env'' : Env + env'' = top-actor-to-back env' actor' : Actor - actor' = add-reference actor newStoreEntry (Return _ ⟶ cont) - valid' : ValidActor newStore actor' - valid' = record { - actor-has-inbox = suc {pr = env .name-supply .supply .name-is-fresh (actor-has-inbox valid)} (actor-has-inbox valid) - ; references-have-pointer = [p: zero ][handles: ⊆-refl ] ∷ ∀map - (λ p → suc-p (env .name-supply .supply .name-is-fresh (actual-has-pointer p)) p) - (references-have-pointer valid) } - env' : Env - env' = record - { acts = newAct ∷ actor' ∷ rest - ; blocked = blocked env - ; store = newStore - ; env-inboxes = [] ∷ env-inboxes env - ; actors-valid = newActValid ∷ valid' ∷ ∀map (valid-actor-suc (env .name-supply .supply)) restValid - ; blocked-valid = ∀map (valid-actor-suc (env .name-supply .supply)) (blocked-valid env) - ; messages-valid = [] ∷ map-suc (store env) (messages-valid env) (env .name-supply .supply) - ; name-supply = env .name-supply .next NewIS - } - where - map-suc : (store : Store) → {store' : Store} {inbs : Inboxes store'} → InboxesValid store inbs → (ns : NameSupply store) → InboxesValid (inbox# ns .name [ NewIS ] ∷ store) inbs - map-suc store [] ns = [] - map-suc store (x ∷ valid) ns = messages-valid-suc ns x ∷ map-suc store valid ns -simulate env | actor ∷ rest | valid ∷ restValid | Send {ToIS = ToIS} canSendTo (SendM tag fields) ⟶ cont = - keep-simulating (Send (name actor) (name foundTo) (reference-names namedFields)) withUnblocked - where - foundTo : FoundReference (store env) ToIS - foundTo = lookup-reference-act valid canSendTo - namedFields = name-fields-act (store env) actor fields valid + actor' = add-reference actor new-store-entry (Return _ ⟶ cont) + valid'' : ValidActor (env'' .store) actor' + valid'' = add-reference-valid RefAdded valid' [p: zero ][handles: ⊆-refl ] + env''' : Env + env''' = replace-focused env'' Focused actor' valid'' + in env''' + +reduce-send : {act : Actor} → (env : Env) → Focus act env → + ActorAtConstructor Send act → + Env +reduce-send env@record { + acts = actor@record { computation = Send {ToIS = ToIS} canSendTo (SendM tag fields) ⟶ cont } ∷ rest + ; actors-valid = actor-valid ∷ rest-valid + } Focused AtSend = + let + to-reference : FoundReference (store env) ToIS + to-reference = lookup-reference-act actor-valid canSendTo + namedFields = name-fields-act (store env) actor fields actor-valid actor' : Actor actor' = replace-actorM actor (Return _ ⟶ cont) withM : Env - withM = replace-actors + withM = replace-focused env - (actor' ∷ rest) - ((rewrap-valid-actor valid refl refl refl) ∷ restValid) + Focused + actor' + (rewrap-valid-actor AreSame actor-valid) + message = NamedM + (translate-message-pointer to-reference tag) + namedFields + message-is-valid : message-valid (env .store) message + message-is-valid = make-pointers-compatible + (env .store) + (actor .pre) + (actor .references) + (actor .pre-eq-refs) + fields + (actor-valid .references-have-pointer) + updater = add-message message message-is-valid withUpdatedInbox : Env withUpdatedInbox = update-inbox-env withM - (underlying-pointer foundTo) - (add-message - (NamedM - (translate-message-pointer foundTo tag) - namedFields) - (make-pointers-compatible - (store env) - (pre actor) - (references actor) - (pre-eq-refs actor) - fields - (references-have-pointer valid))) - withUnblocked : Env - withUnblocked = unblock-actor withUpdatedInbox (name foundTo) -simulate env | actor ∷ rest | valid ∷ restValid | Receive ⟶ cont = keep-simulating (Receive (name actor) (receiveKind (GetInbox.messages actorsInbox))) (env' actorsInbox) - where - actorsInbox : GetInbox (store env) (inbox-shape actor) - actorsInbox = get-inbox env (actor-has-inbox valid) - inboxesAfter = update-inboxes (store env) (env-inboxes env) (messages-valid env) (actor-has-inbox valid) remove-message - receiveKind : List (NamedMessage (inbox-shape actor)) → ReceiveKind - receiveKind [] = Nothing - receiveKind (NamedM _ ps ∷ xs) = Value (reference-names ps) - env' : GetInbox (store env) (inbox-shape actor) → Env - env' record { messages = [] } = replace-actors+blocked - env - rest - restValid - (actor ∷ blocked env) - (valid ∷ blocked-valid env) - env' record { messages = (nm ∷ messages) ; valid = nmv ∷ vms } = record - { acts = add-references-rewrite - actor - (named-inboxes nm) - {unname-message nm} - (add-references++ - nm - nmv - (pre actor)) - (Return (unname-message nm) ⟶ cont) - ∷ rest - ; blocked = blocked env - ; store = store env - ; env-inboxes = updated-inboxes inboxesAfter - ; actors-valid = record { - actor-has-inbox = actor-has-inbox valid - ; references-have-pointer = valid++ - nm - nmv - (references-have-pointer valid) } - ∷ restValid - ; blocked-valid = blocked-valid env - ; messages-valid = inboxes-valid inboxesAfter - ; name-supply = env .name-supply - } -simulate env | actor ∷ rest | valid ∷ restValid | Self ⟶ cont = keep-simulating (Self (name actor)) env' - where + (underlying-pointer to-reference) + updater + in withUpdatedInbox + + +reduce-receive-without-message : {act : Actor} → (env : Env) → Focus act env → + ActorAtConstructor Receive act → + (p : has-inbox (env .store) act) → + inbox-for-actor (env .env-inboxes) act p [] → + Env +reduce-receive-without-message env Focused AtReceive p ifa = block-focused env Focused (BlockedReceive AtReceive p ifa) + +reduce-receive-with-message : {act : Actor} → (env : Env) → Focus act env → + ActorAtConstructor Receive act → + (p : has-inbox (env .store) act) → + ∀ inbox → + all-messages-valid (env .store) inbox → + InboxInState NonEmpty inbox → + inbox-for-actor (env .env-inboxes) act p inbox → + Env +reduce-receive-with-message env@record { + acts = actor@record { computation = (Receive ⟶ cont) } ∷ rest + ; actors-valid = actor-valid ∷ rest-valid + } Focused AtReceive p (nm ∷ messages) (nmv ∷ vms) HasMessage ifa = + let + inboxesAfter = update-inbox + (env .store) + (env .env-inboxes) + (env .messages-valid) + (actor-valid .actor-has-inbox) + remove-message actor' : Actor - actor' = add-reference actor inbox# (name actor) [ (inbox-shape actor) ] (Return _ ⟶ cont) - valid' : ValidActor (store env) actor' - valid' = record { - actor-has-inbox = actor-has-inbox valid - ; references-have-pointer = [p: (actor-has-inbox valid) ][handles: ⊆-refl ] ∷ references-have-pointer valid } + actor' = add-references-rewrite + actor + (named-inboxes nm) + {unname-message nm} + (add-references++ + nm + nmv + (pre actor)) + (Return (unname-message nm) ⟶ cont) + actor-valid' : ValidActor (env .store) actor' + actor-valid' = record { + actor-has-inbox = actor-valid .actor-has-inbox + ; references-have-pointer = valid++ nm nmv (actor-valid .references-have-pointer) + } env' : Env - env' = replace-actors env (actor' ∷ rest) (valid' ∷ restValid) -simulate env | actor ∷ rest | valid ∷ restValid | Strengthen {ys} inc ⟶ cont = keep-simulating (Strengthen (name actor)) env' + env' = let + updated = update-inbox (env .store) (env .env-inboxes) (env .messages-valid) (actor-valid .actor-has-inbox) remove-message + unblock-split = unblock-actors updated (env .blocked) (env .blocked-valid) (env .blocked-no-progress) + open UnblockedActors + in record + { acts = actor' ∷ unblock-split .unblocked ++ rest + ; blocked = unblock-split .still-blocked + ; store = env .store + ; env-inboxes = updated .updated-inboxes + ; name-supply = env .name-supply + ; actors-valid = actor-valid' ∷ ++⁺ (unblock-split .unblocked-valid) rest-valid + ; blocked-valid = unblock-split .blocked-valid + ; messages-valid = updated .inboxes-valid + ; blocked-no-progress = unblock-split .blocked-no-prog + } + in env' + + +reduce-receive : {act : Actor} → (env : Env) → Focus act env → + ActorAtConstructor Receive act → + Env +reduce-receive env@record { acts = actor ∷ rest ; actors-valid = actor-valid ∷ _ } Focused AtReceive = choose-reduction (get-inbox env (actor-valid .actor-has-inbox)) where - liftedRefs = lift-references inc (references actor) (pre-eq-refs actor) - strengthenedM : ActorM ∞ (inbox-shape actor) ⊤₁ (map shape (contained liftedRefs)) (λ _ → ys) - strengthenedM rewrite (sym (contained-eq-inboxes liftedRefs))= Return _ + open GetInbox + choose-reduction : (gi : GetInbox (env .store) (env .env-inboxes) (actor-valid .actor-has-inbox)) → Env + choose-reduction gi@record { messages = [] } = + reduce-receive-without-message env Focused AtReceive _ (gi .right-inbox) + choose-reduction gi@record { messages = _ ∷ _ } = + reduce-receive-with-message env Focused AtReceive _ (gi .messages) (gi .valid) HasMessage (gi .right-inbox) + +reduce-self : {act : Actor} → (env : Env) → Focus act env → + ActorAtConstructor Self act → + Env +reduce-self env@record { acts = actor@record { + computation = Self ⟶ cont } ∷ _ + ; actors-valid = actor-valid ∷ _ + } Focused AtSelf = + let actor' : Actor - actor' = lift-actor actor (contained liftedRefs) refl (strengthenedM ⟶ cont) - valid' : ValidActor (store env) actor' - valid' = record { - actor-has-inbox = actor-has-inbox valid - ; references-have-pointer = All-⊆ (subset liftedRefs) (references-have-pointer valid) } + actor' = add-reference actor inbox# (actor .name) [ (actor .inbox-shape) ] ((Return _) ⟶ cont) + actor-valid' : ValidActor (env .store) actor' + actor-valid' = add-reference-valid RefAdded actor-valid [p: (actor-valid .actor-has-inbox) ][handles: ⊆-refl ] env' : Env - env' = replace-actors env (actor' ∷ rest) (valid' ∷ restValid) + env' = replace-focused + env + Focused + actor' + actor-valid' + in env' +reduce-strengthen : {act : Actor} → (env : Env) → Focus act env → + ActorAtConstructor Strengthen act → + Env +reduce-strengthen env@record { + acts = actor@record { computation = Strengthen {ys} inc ⟶ cont } ∷ _ + ; actors-valid = actor-valid ∷ _ + } Focused AtStrengthen = + let + lifted-references = lift-references inc (references actor) (pre-eq-refs actor) + actor' : Actor + actor' = lift-actor actor (lifted-references .contained) (lifted-references .contained-eq-inboxes) (Return _ ⟶ cont) + actor-valid' : ValidActor (env .store) actor' + actor-valid' = lift-valid-actor (CanBeLifted lifted-references) actor-valid + env' : Env + env' = replace-focused + env + Focused + actor' + actor-valid' + in env' + +reduce : {act : Actor} → (env : Env) → Focus act env → Env +reduce env@record { acts = record { computation = (Return val ⟶ []) } ∷ _ } Focused = + reduce-unbound-return env Focused AtReturn (NoContinuation {v = val}) +reduce env@record { acts = record { computation = (Return val ⟶ (_ ∷ _)) } ∷ _ } Focused = + reduce-bound-return env Focused AtReturn (HasContinuation {v = val}) +reduce env@record { acts = record { computation = ((m ∞>>= f) ⟶ _)} ∷ _ } Focused = + reduce-bind env Focused AtBind +reduce env@record { acts = record { computation = (Spawn act ⟶ cont) } ∷ _ } Focused = + reduce-spawn env Focused AtSpawn +reduce env@record { acts = record { computation = (Send canSendTo msg ⟶ cont) } ∷ _ } Focused = + reduce-send env Focused AtSend +reduce env@record { acts = record { computation = (Receive ⟶ cont) } ∷ _ } Focused = + reduce-receive env Focused AtReceive +reduce env@record { acts = record { computation = (Self ⟶ cont) } ∷ _ } Focused = + reduce-self env Focused AtSelf +reduce env@record { acts = record { computation = (Strengthen inc ⟶ cont) } ∷ _ } Focused = + reduce-strengthen env Focused AtStrengthen -keep-simulating trace env .force = record { env = env ; trace = trace } ∷ simulate (top-actor-to-back env) +simulate : Env → ∞Trace ∞ +simulate env@record { acts = [] ; actors-valid = [] } = delay TraceStop env AllBlocked +simulate env@record { acts = _ ∷ _ ; actors-valid = _ ∷ _ } = keep-stepping (reduce env Focused) + where + open ∞Trace + keep-stepping : Env → ∞Trace ∞ + keep-stepping env .force = env ∷ simulate env diff --git a/src/SimulationEnvironment.agda b/src/SimulationEnvironment.agda index e96f3d8..b08c11b 100644 --- a/src/SimulationEnvironment.agda +++ b/src/SimulationEnvironment.agda @@ -1,6 +1,7 @@ module SimulationEnvironment where -open import Membership using (_∈_ ; find-∈) +open import Membership using (_∈_ ; find-∈ ; _⊆_) open import ActorMonad +open import NatProps open import Data.List using (List ; _∷_ ; [] ; map) open import Data.List.All using (All ; _∷_ ; [] ; lookup) renaming (map to ∀map) @@ -17,6 +18,7 @@ open import Relation.Nullary using (Dec ; yes ; no ; ¬_) open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym) open import Relation.Unary using (Decidable) renaming (_⊆_ to _⋐_) + -- We give every actor and inbox a name. -- The internal type of an actor is not important, -- but the type needs to have an easy way of creating @@ -48,15 +50,6 @@ record NamedInbox : Set₁ where -- Inserting duplicate keys is thus pointless and is not done anywhere in the code. Store = List NamedInbox --- Decidable inequality -¬[_] : ∀ {a b : Name} → Dec (a ≡ b) → Set -¬[ (yes x₁) ] = ⊥ -¬[ (no x₁) ] = ⊤ - --- Also decidable inequality -_¬≡_ : ( a b : Name) → Set -a ¬≡ b = ¬[ a ≟ b ] - -- A pointer into the store. -- This is a proof that the name points to an inbox shape in the store. -- The store is a key-value list that returns the first value matching the key (name). @@ -66,7 +59,7 @@ a ¬≡ b = ¬[ a ≟ b ] data _↦_∈e_ (n : Name) (S : InboxShape) : Store → Set where zero : ∀ {xs} → n ↦ S ∈e (inbox# n [ S ] ∷ xs) - suc : ∀ {n' : Name} { S' xs} {pr : n ¬≡ n'} + suc : ∀ {n' : Name} { S' xs} {pr : ¬ n ≡ n'} → n ↦ S ∈e xs → n ↦ S ∈e (inbox# n' [ S' ] ∷ xs) @@ -129,23 +122,46 @@ named-field-content (ReferenceType Fw) = Name -- The decision to use names for references and pointers, rather than just ∈, -- makes it possible to prove that a sent message containing a reference -- does not need to be modified when more actors are added. -data NamedMessage (To : InboxShape): Set₁ where - NamedM : {MT : MessageType} → MT ∈ To → All named-field-content MT → NamedMessage To +record NamedMessage (To : InboxShape): Set₁ where + constructor NamedM + field + {MT} : MessageType + named-message-type : MT ∈ To + named-fields : All named-field-content MT + +unname-message : ∀ {S} → NamedMessage S → Message S +unname-message (NamedM x fields) = Msg x (do-the-work fields) + where + do-the-work : ∀ {MT} → All named-field-content MT → All receive-field-content MT + do-the-work {[]} nfc = [] + do-the-work {ValueType x₁ ∷ MT} (px ∷ nfc) = px ∷ (do-the-work nfc) + do-the-work {ReferenceType x₁ ∷ MT} (px ∷ nfc) = _ ∷ do-the-work nfc Inbox : InboxShape → Set₁ Inbox is = List (NamedMessage is) data Inboxes : (store : Store) → Set₁ where [] : Inboxes [] - _∷_ : ∀ {store name inbox-shape} → List (NamedMessage inbox-shape) → + _∷_ : ∀ {store name inbox-shape} → Inbox inbox-shape → (inboxes : Inboxes store) → Inboxes (inbox# name [ inbox-shape ] ∷ store) +data InboxForPointer {inbox-shape : InboxShape} (inbox : Inbox inbox-shape) {name : Name} : (store : Store) → (Inboxes store) → (name ↦ inbox-shape ∈e store) → Set₁ where + zero : ∀ {store} {inbs : Inboxes store} → + InboxForPointer inbox (inbox# name [ inbox-shape ] ∷ store) (inbox ∷ inbs) zero + suc : ∀ {n' : Name} {S' inb' store} {p : name ↦ inbox-shape ∈e store} {inbs : Inboxes store} {pr : ¬ name ≡ n'} → + InboxForPointer inbox store inbs p → + InboxForPointer inbox (inbox# n' [ S' ] ∷ store) (inb' ∷ inbs) (suc {pr = pr} p) + -- Property that there exists an inbox of the right shape in the list of inboxes -- This is used both for proving that every actor has an inbox, -- and for proving that every reference known by an actor has an inbox has-inbox : Store → Actor → Set has-inbox store actor = Actor.name actor ↦ Actor.inbox-shape actor ∈e store + +inbox-for-actor : ∀ {store} (inbs : Inboxes store) (actor : Actor) (p : has-inbox store actor) (inb : Inbox (Actor.inbox-shape actor)) → Set₁ +inbox-for-actor {store} inbs actor p inb = InboxForPointer inb store inbs p + reference-has-pointer : Store → NamedInbox → Set₁ reference-has-pointer store ni = name ni comp↦ shape ni ∈ store where open NamedInbox @@ -200,27 +216,16 @@ NameFresh : Store → ℕ → Set₁ NameFresh store n = All (λ v → name v Data.Nat.< n) store where open NamedInbox - --- convert < to ¬≡ -<-¬≡ : ∀ {n m} → n < m → n ¬≡ m -<-¬≡ {zero} {zero} () -<-¬≡ {zero} {suc m} p = _ -<-¬≡ {suc n} {zero} () -<-¬≡ {suc n} {suc m} (Data.Nat.s≤s p) with (<-¬≡ p) -... | q with (n ≟ m) -<-¬≡ {suc n} {suc m} (Data.Nat.s≤s p) | () | yes p₁ -<-¬≡ {suc n} {suc m} (Data.Nat.s≤s p) | q | no ¬p = _ - -- If a name is fresh for a store (i.e. all names in the store are < than the name), -- then none of the names in the store is equal to the name -Fresh¬≡ : ∀ {store name } → NameFresh store name → (All (λ m → (NamedInbox.name m) ¬≡ name) store) +Fresh¬≡ : ∀ {store name } → NameFresh store name → (All (λ m → ¬ (NamedInbox.name m) ≡ name) store) Fresh¬≡ ls = ∀map (λ frsh → <-¬≡ frsh) ls record NameSupply (store : Store) : Set₁ where field name : Name freshness-carrier : All (λ v → NamedInbox.name v < name) store - name-is-fresh : {n : Name} {IS : InboxShape} → n ↦ IS ∈e store → ¬[ n ≟ name ] + name-is-fresh : {n : Name} {IS : InboxShape} → n ↦ IS ∈e store → ¬ n ≡ name open NameSupply @@ -236,11 +241,11 @@ record NameSupplyStream (i : Size) (store : Store) : Set₁ where suc-helper : ∀ {store name IS n} → name ↦ IS ∈e store → All (λ v → suc (NamedInbox.name v) Data.Nat.≤ n) store → - ¬[ name ≟ n ] + ¬ name ≡ n suc-helper zero (px ∷ p) = <-¬≡ px suc-helper (suc q) (px ∷ p) = suc-helper q p -suc-p : ∀ {store name n x shape} → ¬[ name ≟ n ] → name comp↦ shape ∈ store → name comp↦ shape ∈ (inbox# n [ x ] ∷ store) +suc-p : ∀ {store name n x shape} → ¬ name ≡ n → name comp↦ shape ∈ store → name comp↦ shape ∈ (inbox# n [ x ] ∷ store) suc-p pr [p: actual-has-pointer ][handles: actual-handles-wanted ] = [p: (suc {pr = pr} actual-has-pointer) ][handles: actual-handles-wanted ] open NameSupplyStream @@ -266,25 +271,188 @@ name-supply-singleton .next = stream-builder (name-supply-singleton .supply) stream-builder ns IS .supply = next-name-supply ns IS stream-builder ns IS .next = stream-builder (next-name-supply ns IS) +data ActorConstructor : Set where + Return : ActorConstructor + Bind : ActorConstructor + Spawn : ActorConstructor + Send : ActorConstructor + Receive : ActorConstructor + Self : ActorConstructor + Strengthen : ActorConstructor + +data ActorAtConstructor : ActorConstructor → Actor → Set₂ where + AtReturn : + ∀ {IS A B refs mid post name} + {cont : ContStack ∞ IS mid post} + {v : A} + {per} → + ActorAtConstructor Return (record + { inbox-shape = IS + ; A = B + ; references = refs + ; pre = mid v + ; pre-eq-refs = per + ; post = post + ; computation = Return v ⟶ cont + ; name = name + }) + AtBind : + ∀ {IS A B C refs pre mid name} + {m : ∞ActorM ∞ IS A pre mid} + {post : B → TypingContext} + {f : (x : A) → + ∞ActorM ∞ IS B (mid x) post} + {contpost : C → TypingContext} + {cont : ContStack ∞ IS post contpost} → + ∀ {per} → + ActorAtConstructor Bind (record + { inbox-shape = IS + ; A = C + ; references = refs + ; pre = pre + ; pre-eq-refs = per + ; post = contpost + ; computation = (m ∞>>= f) ⟶ cont + ; name = name + }) + AtSpawn : + ∀ {IS NewIS A B refs pre post postN name} + {m : ActorM ∞ NewIS A [] postN} + {cont : ContStack ∞ IS (λ _ → NewIS ∷ pre) post} + {per} → + ActorAtConstructor Spawn (record + { inbox-shape = IS + ; A = B + ; references = refs + ; pre = pre + ; pre-eq-refs = per + ; post = post + ; computation = Spawn m ⟶ cont + ; name = name + }) + AtSend : + ∀ {IS ToIS A refs pre post name} + {canSendTo : pre ⊢ ToIS} + {msg : SendMessage ToIS pre} + {cont : ContStack ∞ IS (λ _ → pre) post} + {per} → + ActorAtConstructor Send (record + { inbox-shape = IS + ; A = A + ; references = refs + ; pre = pre + ; pre-eq-refs = per + ; post = post + ; computation = (Send canSendTo msg) ⟶ cont + ; name = name + }) + AtReceive : + ∀ {IS A refs pre post name} + {cont : ContStack ∞ IS (add-references pre) post} + {per} → + ActorAtConstructor Receive (record + { inbox-shape = IS + ; A = A + ; references = refs + ; pre = pre + ; pre-eq-refs = per + ; post = post + ; computation = Receive ⟶ cont + ; name = name + }) + AtSelf : + ∀ {IS A refs pre post name} + {cont : ContStack ∞ IS (λ _ → IS ∷ pre) post} + {per} → + ActorAtConstructor Self (record + { inbox-shape = IS + ; A = A + ; references = refs + ; pre = pre + ; pre-eq-refs = per + ; post = post + ; computation = Self ⟶ cont + ; name = name + }) + AtStrengthen : + ∀ {IS A refs ys xs post name} + {inc : ys ⊆ xs} + {cont : ContStack ∞ IS (λ _ → ys) post} + {per} → + ActorAtConstructor Strengthen (record + { inbox-shape = IS + ; A = A + ; references = refs + ; pre = xs + ; pre-eq-refs = per + ; post = post + ; computation = (Strengthen inc) ⟶ cont + ; name = name + }) + +data ActorHasContinuation : Actor → Set₂ where + HasContinuation : + ∀ {IS A B C refs pre mid contmid post name} + {m : ActorM ∞ IS A pre mid} + {f : Cont ∞ IS {A} {B} mid contmid} + {cont : ContStack ∞ IS contmid post} + {v : A} + {per} → + ActorHasContinuation (record + { inbox-shape = IS + ; A = C + ; references = refs + ; pre = pre + ; pre-eq-refs = per + ; post = post + ; computation = m ⟶ (f ∷ cont) + ; name = name + }) + +data ActorHasNoContinuation : Actor → Set₂ where + NoContinuation : + ∀ {IS A refs pre post name} + {m : ActorM ∞ IS A pre post} + {v : A} + {per} → + ActorHasNoContinuation (record + { inbox-shape = IS + ; A = A + ; references = refs + ; pre = pre + ; pre-eq-refs = per + ; post = post + ; computation = m ⟶ [] + ; name = name + }) + +data IsBlocked (store : Store) (inbs : Inboxes store) (actor : Actor) : Set₂ where + BlockedReturn : + ActorAtConstructor Return actor → + ActorHasNoContinuation actor → + IsBlocked store inbs actor + BlockedReceive : + ActorAtConstructor Receive actor → + (p : has-inbox store actor) → + InboxForPointer [] store inbs p → + IsBlocked store inbs actor + -- The environment is a list of actors and inboxes, -- with a proof that every ector is valid in the context of said list of inboxes record Env : Set₂ where field - -- The currently active actors + -- raw acts : List Actor - -- The currently blocked actors, i.e. actors doing receive without any messages in its inbox. - -- By separating blocked and non-blocked actors we both optimize the simulation to not try to run - -- actors that won't succed in taking a step, and we get a clear step-condition when there are no - -- non-blocked actors left. blocked : List Actor store : Store env-inboxes : Inboxes store - -- The proofs that an actor and a blocked actor is valid is actually the same proof, - -- but kept in a separate list. + name-supply : NameSupplyStream ∞ store + -- coherence actors-valid : All (ValidActor store) acts blocked-valid : All (ValidActor store) blocked messages-valid : InboxesValid store env-inboxes - name-supply : NameSupplyStream ∞ store + -- weak progress + blocked-no-progress : All (IsBlocked store env-inboxes) blocked -- The empty environment empty-env : Env @@ -297,6 +465,7 @@ empty-env = record ; blocked-valid = [] ; messages-valid = [] ; name-supply = name-supply-singleton + ; blocked-no-progress = [] } -- An environment containing a single actor. @@ -320,4 +489,51 @@ singleton-env {IS} {A} {post} actor = record ; blocked-valid = [] ; messages-valid = [] ∷ [] ; name-supply = name-supply-singleton .next IS + ; blocked-no-progress = [] } + + +data Focus (act : Actor) : Env → Set₂ where + Focused : + {rest : List Actor} + {bl : List Actor} + {str : Store} + {inbs : Inboxes str} + {rv : All (ValidActor str) rest} + {bv : All (ValidActor str) bl} + {bib : All (IsBlocked str inbs) bl} + {mv : InboxesValid str inbs} + {ns : NameSupplyStream ∞ str} + {va : ValidActor str act} → + Focus act (record + { acts = act ∷ rest + ; blocked = bl + ; store = str + ; env-inboxes = inbs + ; actors-valid = va ∷ rv + ; blocked-valid = bv + ; messages-valid = mv + ; name-supply = ns + ; blocked-no-progress = bib + }) + +data Done : Env → Set₂ where + AllBlocked : + {bl : List Actor} + {str : Store} + {inbs : Inboxes str} + {bv : All (ValidActor str) bl} + {bib : All (IsBlocked str inbs) bl} + {mv : InboxesValid str inbs} + {ns : NameSupplyStream ∞ str} → + Done (record + { acts = [] + ; blocked = bl + ; store = str + ; env-inboxes = inbs + ; name-supply = ns + ; actors-valid = [] + ; blocked-valid = bv + ; messages-valid = mv + ; blocked-no-progress = bib + })