From 6739fbbe5342fbef8f8f59b6461865fd186c502c Mon Sep 17 00:00:00 2001 From: Pierre Krafft Date: Wed, 4 Apr 2018 20:05:28 +0200 Subject: [PATCH] Convert fresh name into name supply --- src/EnvironmentOperations.agda | 89 ++++++++---------------- src/Selective/EnvironmentOperations.agda | 89 ++++++++---------------- src/Selective/Simulate.agda | 35 +++++----- src/Selective/SimulationEnvironment.agda | 84 +++++++++++++++++++--- src/Simulate.agda | 32 ++++----- src/SimulationEnvironment.agda | 84 +++++++++++++++++++--- 6 files changed, 234 insertions(+), 179 deletions(-) diff --git a/src/EnvironmentOperations.agda b/src/EnvironmentOperations.agda index 817dde6..b5b746c 100644 --- a/src/EnvironmentOperations.agda +++ b/src/EnvironmentOperations.agda @@ -24,6 +24,7 @@ open Actor open ValidActor open Env open NamedInbox +open NameSupplyStream -- We can create a new Actor from an ActorM if we know its name. -- This is used when spawning an actor. @@ -98,7 +99,6 @@ add-references-to-actor actor nms m = record ; computation = m ; name = name actor } - add-references-rewrite : (actor : Actor) → (nms : List NamedInbox) → {x : Message (inbox-shape actor)} → map shape nms ++ pre actor ≡ add-references (pre actor) x → ActorState ∞ (inbox-shape actor) (A actor) (add-references (pre actor) x) (post actor) → @@ -139,6 +139,7 @@ record UpdatedInboxes (store : Store) {store' : Store} (original : Inboxes stor open ValidMessageList open UpdatedInboxes +open NameSupply -- Update one of the inboxes in a list of inboxes. -- All the inboxes have been proven to be valid in the context of a store, @@ -173,11 +174,10 @@ top-actor-to-back env | x ∷ acts | (y ∷ prfs) = record ; blocked = blocked env ; env-inboxes = env-inboxes env ; store = store env - ; fresh-name = fresh-name env ; actors-valid = ++⁺ prfs (y ∷ []) ; blocked-valid = blocked-valid env ; messages-valid = messages-valid env - ; name-is-fresh = name-is-fresh env + ; name-supply = name-supply env } -- Drop the actor that is at the top of the list completely. @@ -191,62 +191,35 @@ drop-top-actor env | _ ∷ rest | _ ∷ prfs = record ; blocked = blocked env ; env-inboxes = env-inboxes env ; store = store env - ; fresh-name = fresh-name env ; actors-valid = prfs ; blocked-valid = blocked-valid env ; messages-valid = messages-valid env - ; name-is-fresh = name-is-fresh env + ; name-supply = name-supply env } --- 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¬≡ ls = ∀map (λ frsh → <-¬≡ frsh) ls - --- helps show that all the names in the store are still valid if we add a new name on top, --- if the new name is > than all the names already in the store. -suc-helper : ∀ {store name IS n} → - name ↦ IS ∈e store → - All (λ v → suc (NamedInbox.name v) Data.Nat.≤ n) store → - ¬[ 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 pr [p: actual-has-pointer ][handles: actual-handles-wanted ] = [p: (suc {pr = pr} actual-has-pointer) ][handles: actual-handles-wanted ] - -- 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 n x} → (NameFresh store n) → ValidActor store actor → ValidActor (inbox# n [ x ] ∷ store) actor -valid-actor-suc frsh va = record { - actor-has-inbox = suc {pr = suc-helper (actor-has-inbox va) frsh} (actor-has-inbox va) - ; references-have-pointer = ∀map (λ p → suc-p (suc-helper (actual-has-pointer p) frsh) p) (references-have-pointer va) } -- suc-p (suc-helper p frsh) p +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↦_∈_ -- 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 n x} {inb : Inbox IS} → (NameFresh store n) → all-messages-valid store inb → all-messages-valid (inbox# n [ x ] ∷ store) inb -messages-valid-suc {store} {IS} {n} {x} frsh [] = [] -messages-valid-suc {store} {IS} {n} {x} {nx ∷ _} frsh (px ∷ vi) = message-valid-suc nx px ∷ (messages-valid-suc frsh vi) +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 +messages-valid-suc {store} {IS} {x} ns [] = [] +messages-valid-suc {store} {IS} {x} {nx ∷ _} ns (px ∷ vi) = message-valid-suc nx px ∷ (messages-valid-suc ns vi) where open _comp↦_∈_ fields-valid-suc : ∀ {MT} {fields : All named-field-content MT} → FieldsHavePointer store fields → - FieldsHavePointer (inbox# n [ x ] ∷ store) fields + FieldsHavePointer (inbox# ns .name [ x ] ∷ store) fields fields-valid-suc [] = [] fields-valid-suc (FhpV ∷ valid) = FhpV ∷ fields-valid-suc valid - fields-valid-suc (FhpR x ∷ valid) = FhpR (suc-p (suc-helper (actual-has-pointer x) frsh) x) ∷ (fields-valid-suc valid) - message-valid-suc : (nx : NamedMessage IS) → message-valid store nx → message-valid (inbox# n [ x ] ∷ store) nx + fields-valid-suc (FhpR x ∷ valid) = FhpR (suc-p (ns .name-is-fresh (actual-has-pointer x)) x) ∷ (fields-valid-suc valid) + 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 -- Add a new actor to the environment. @@ -261,21 +234,20 @@ add-top {IS} {A} {post} m env = record ; pre-eq-refs = refl ; post = post ; computation = m - ; name = fresh-name env + ; name = env .name-supply .supply .name } ∷ acts env ; blocked = blocked env ; env-inboxes = [] ∷ env-inboxes env - ; store = inbox# fresh-name env [ IS ] ∷ store env - ; fresh-name = suc (fresh-name env) - ; actors-valid = record { actor-has-inbox = zero ; references-have-pointer = [] } ∷ ∀map (valid-actor-suc (name-is-fresh env)) (actors-valid env) - ; blocked-valid = ∀map (valid-actor-suc (name-is-fresh env)) (blocked-valid env) - ; messages-valid = [] ∷ map-suc (store env) (messages-valid env) (name-is-fresh env) - ; name-is-fresh = Data.Nat.s≤s (≤-reflexive refl) ∷ ∀map Data.Nat.Properties.≤-step (name-is-fresh env) + ; store = inbox# env .name-supply .supply .name [ IS ] ∷ store env + ; actors-valid = record { actor-has-inbox = zero ; references-have-pointer = [] } ∷ ∀map (valid-actor-suc (env .name-supply .supply)) (actors-valid env) + ; 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 } where - map-suc : (store : Store) → {store' : Store} → {inbs : Inboxes store'} → InboxesValid store inbs → ∀ {n} → (NameFresh store n) → InboxesValid (inbox# n [ IS ] ∷ store) inbs - map-suc store [] frsh = [] - map-suc store (x ∷ valid) frsh = messages-valid-suc frsh x ∷ (map-suc store valid frsh) + 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 field @@ -301,11 +273,10 @@ update-inbox-env {name} {IS} env p f = record ; blocked = blocked env ; env-inboxes = updated-inboxes updated ; store = store env - ; fresh-name = fresh-name env ; actors-valid = actors-valid env ; blocked-valid = blocked-valid env ; messages-valid = inboxes-valid updated - ; name-is-fresh = name-is-fresh env + ; name-supply = env .name-supply } where updated = update-inboxes (store env) (env-inboxes env) (messages-valid env) p f @@ -331,11 +302,10 @@ unblock-actor env name = newEnv (loop (blocked env) (blocked-valid env)) ; blocked = ba ; env-inboxes = env-inboxes env ; store = store env - ; fresh-name = fresh-name env ; actors-valid = ++⁺ (actors-valid env) unblockedValid ; blocked-valid = baValid ; messages-valid = messages-valid env - ; name-is-fresh = name-is-fresh env + ; name-supply = env .name-supply } record FoundReference (store : Store) (S : InboxShape) : Set₂ where @@ -407,11 +377,10 @@ replace-actors env actors actorsValid = record { ; blocked = blocked env ; env-inboxes = env-inboxes env ; store = store env - ; fresh-name = fresh-name env ; actors-valid = actorsValid ; blocked-valid = blocked-valid env ; messages-valid = messages-valid env - ; name-is-fresh = name-is-fresh env + ; name-supply = env .name-supply } -- We can replace both the running and blocked actors in an environment if they all are valid for the current store. @@ -423,11 +392,10 @@ replace-actors+blocked env actors actorsValid blocked blockedValid = record { ; blocked = blocked ; env-inboxes = env-inboxes env ; store = store env - ; fresh-name = fresh-name env ; actors-valid = actorsValid ; blocked-valid = blockedValid ; messages-valid = messages-valid env - ; name-is-fresh = name-is-fresh env + ; name-supply = env .name-supply } -- Takes a named message and a proof that the named message is valid for the store. @@ -537,3 +505,4 @@ make-pointers-compatible store _ refs refl (_∷_ {ReferenceType x} px fields) r where foundFw : FoundReference store (actual px) foundFw = lookup-reference _ refs rhp refl (actual-is-sendable px) + diff --git a/src/Selective/EnvironmentOperations.agda b/src/Selective/EnvironmentOperations.agda index 16fb36c..f55cbcb 100644 --- a/src/Selective/EnvironmentOperations.agda +++ b/src/Selective/EnvironmentOperations.agda @@ -25,6 +25,7 @@ open Actor open ValidActor open Env open NamedInbox +open NameSupplyStream -- We can create a new Actor from an ActorM if we know its name. -- This is used when spawning an actor. @@ -99,7 +100,6 @@ add-references-to-actor actor nms m = record ; computation = m ; name = name actor } - add-references-rewrite : (actor : Actor) → (nms : List NamedInbox) → {x : Message (inbox-shape actor)} → map shape nms ++ pre actor ≡ add-references (pre actor) x → ActorState ∞ (inbox-shape actor) (A actor) (add-references (pre actor) x) (post actor) → @@ -140,6 +140,7 @@ record UpdatedInboxes (store : Store) {store' : Store} (original : Inboxes stor open ValidMessageList open UpdatedInboxes +open NameSupply -- Update one of the inboxes in a list of inboxes. -- All the inboxes have been proven to be valid in the context of a store, @@ -174,11 +175,10 @@ top-actor-to-back env | x ∷ acts | (y ∷ prfs) = record ; blocked = blocked env ; env-inboxes = env-inboxes env ; store = store env - ; fresh-name = fresh-name env ; actors-valid = ++⁺ prfs (y ∷ []) ; blocked-valid = blocked-valid env ; messages-valid = messages-valid env - ; name-is-fresh = name-is-fresh env + ; name-supply = name-supply env } -- Drop the actor that is at the top of the list completely. @@ -192,62 +192,35 @@ drop-top-actor env | _ ∷ rest | _ ∷ prfs = record ; blocked = blocked env ; env-inboxes = env-inboxes env ; store = store env - ; fresh-name = fresh-name env ; actors-valid = prfs ; blocked-valid = blocked-valid env ; messages-valid = messages-valid env - ; name-is-fresh = name-is-fresh env + ; name-supply = name-supply env } --- 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¬≡ ls = ∀map (λ frsh → <-¬≡ frsh) ls - --- helps show that all the names in the store are still valid if we add a new name on top, --- if the new name is > than all the names already in the store. -suc-helper : ∀ {store name IS n} → - name ↦ IS ∈e store → - All (λ v → suc (NamedInbox.name v) Data.Nat.≤ n) store → - ¬[ 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 pr [p: actual-has-pointer ][handles: actual-handles-wanted ] = [p: (suc {pr = pr} actual-has-pointer) ][handles: actual-handles-wanted ] - -- 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 n x} → (NameFresh store n) → ValidActor store actor → ValidActor (inbox# n [ x ] ∷ store) actor -valid-actor-suc frsh va = record { - actor-has-inbox = suc {pr = suc-helper (actor-has-inbox va) frsh} (actor-has-inbox va) - ; references-have-pointer = ∀map (λ p → suc-p (suc-helper (actual-has-pointer p) frsh) p) (references-have-pointer va) } -- suc-p (suc-helper p frsh) p +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↦_∈_ -- 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 n x} {inb : Inbox IS} → (NameFresh store n) → all-messages-valid store inb → all-messages-valid (inbox# n [ x ] ∷ store) inb -messages-valid-suc {store} {IS} {n} {x} frsh [] = [] -messages-valid-suc {store} {IS} {n} {x} {nx ∷ _} frsh (px ∷ vi) = message-valid-suc nx px ∷ (messages-valid-suc frsh vi) +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 +messages-valid-suc {store} {IS} {x} ns [] = [] +messages-valid-suc {store} {IS} {x} {nx ∷ _} ns (px ∷ vi) = message-valid-suc nx px ∷ (messages-valid-suc ns vi) where open _comp↦_∈_ fields-valid-suc : ∀ {MT} {fields : All named-field-content MT} → FieldsHavePointer store fields → - FieldsHavePointer (inbox# n [ x ] ∷ store) fields + FieldsHavePointer (inbox# ns .name [ x ] ∷ store) fields fields-valid-suc [] = [] fields-valid-suc (FhpV ∷ valid) = FhpV ∷ fields-valid-suc valid - fields-valid-suc (FhpR x ∷ valid) = FhpR (suc-p (suc-helper (actual-has-pointer x) frsh) x) ∷ (fields-valid-suc valid) - message-valid-suc : (nx : NamedMessage IS) → message-valid store nx → message-valid (inbox# n [ x ] ∷ store) nx + fields-valid-suc (FhpR x ∷ valid) = FhpR (suc-p (ns .name-is-fresh (actual-has-pointer x)) x) ∷ (fields-valid-suc valid) + 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 -- Add a new actor to the environment. @@ -262,21 +235,20 @@ add-top {IS} {A} {post} m env = record ; pre-eq-refs = refl ; post = post ; computation = m - ; name = fresh-name env + ; name = env .name-supply .supply .name } ∷ acts env ; blocked = blocked env ; env-inboxes = [] ∷ env-inboxes env - ; store = inbox# fresh-name env [ IS ] ∷ store env - ; fresh-name = suc (fresh-name env) - ; actors-valid = record { actor-has-inbox = zero ; references-have-pointer = [] } ∷ ∀map (valid-actor-suc (name-is-fresh env)) (actors-valid env) - ; blocked-valid = ∀map (valid-actor-suc (name-is-fresh env)) (blocked-valid env) - ; messages-valid = [] ∷ map-suc (store env) (messages-valid env) (name-is-fresh env) - ; name-is-fresh = Data.Nat.s≤s (≤-reflexive refl) ∷ ∀map Data.Nat.Properties.≤-step (name-is-fresh env) + ; store = inbox# env .name-supply .supply .name [ IS ] ∷ store env + ; actors-valid = record { actor-has-inbox = zero ; references-have-pointer = [] } ∷ ∀map (valid-actor-suc (env .name-supply .supply)) (actors-valid env) + ; 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 } where - map-suc : (store : Store) → {store' : Store} → {inbs : Inboxes store'} → InboxesValid store inbs → ∀ {n} → (NameFresh store n) → InboxesValid (inbox# n [ IS ] ∷ store) inbs - map-suc store [] frsh = [] - map-suc store (x ∷ valid) frsh = messages-valid-suc frsh x ∷ (map-suc store valid frsh) + 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 field @@ -302,11 +274,10 @@ update-inbox-env {name} {IS} env p f = record ; blocked = blocked env ; env-inboxes = updated-inboxes updated ; store = store env - ; fresh-name = fresh-name env ; actors-valid = actors-valid env ; blocked-valid = blocked-valid env ; messages-valid = inboxes-valid updated - ; name-is-fresh = name-is-fresh env + ; name-supply = env .name-supply } where updated = update-inboxes (store env) (env-inboxes env) (messages-valid env) p f @@ -332,11 +303,10 @@ unblock-actor env name = newEnv (loop (blocked env) (blocked-valid env)) ; blocked = ba ; env-inboxes = env-inboxes env ; store = store env - ; fresh-name = fresh-name env ; actors-valid = ++⁺ (actors-valid env) unblockedValid ; blocked-valid = baValid ; messages-valid = messages-valid env - ; name-is-fresh = name-is-fresh env + ; name-supply = env .name-supply } record FoundReference (store : Store) (S : InboxShape) : Set₂ where @@ -408,11 +378,10 @@ replace-actors env actors actorsValid = record { ; blocked = blocked env ; env-inboxes = env-inboxes env ; store = store env - ; fresh-name = fresh-name env ; actors-valid = actorsValid ; blocked-valid = blocked-valid env ; messages-valid = messages-valid env - ; name-is-fresh = name-is-fresh env + ; name-supply = env .name-supply } -- We can replace both the running and blocked actors in an environment if they all are valid for the current store. @@ -424,11 +393,10 @@ replace-actors+blocked env actors actorsValid blocked blockedValid = record { ; blocked = blocked ; env-inboxes = env-inboxes env ; store = store env - ; fresh-name = fresh-name env ; actors-valid = actorsValid ; blocked-valid = blockedValid ; messages-valid = messages-valid env - ; name-is-fresh = name-is-fresh env + ; name-supply = env .name-supply } -- Takes a named message and a proof that the named message is valid for the store. @@ -539,7 +507,6 @@ make-pointers-compatible store _ refs refl (_∷_ {ReferenceType x} px fields) r 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 diff --git a/src/Selective/Simulate.agda b/src/Selective/Simulate.agda index 635b15d..2c5764b 100644 --- a/src/Selective/Simulate.agda +++ b/src/Selective/Simulate.agda @@ -53,6 +53,8 @@ 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. @@ -83,25 +85,23 @@ simulate env | actor ∷ rest | valid ∷ restValid | (m ∞>>= f) ⟶ cont = ke 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) (fresh-name env)) env' +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# (fresh-name env) [ NewIS ] + newStoreEntry = inbox# (env .name-supply .supply .name) [ NewIS ] newStore : Store newStore = newStoreEntry ∷ store env newAct : Actor - newAct = new-actor act (fresh-name env) + newAct = new-actor act (env .name-supply .supply .name) newActValid : ValidActor newStore newAct newActValid = record { actor-has-inbox = zero ; references-have-pointer = [] } - newIsFresh : NameFresh newStore (suc (fresh-name env)) - newIsFresh = s≤s (≤-reflexive refl) ∷ ∀map ≤-step (name-is-fresh env) actor' : Actor actor' = add-reference actor newStoreEntry (Return _ ⟶ cont) valid' : ValidActor newStore actor' valid' = record { - actor-has-inbox = suc {pr = suc-helper (actor-has-inbox valid) (name-is-fresh env)} (actor-has-inbox valid) + 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 (suc-helper (actual-has-pointer p) (name-is-fresh env)) p) + (λ p → suc-p (env .name-supply .supply .name-is-fresh (actual-has-pointer p)) p) (references-have-pointer valid) } env' : Env env' = record @@ -109,16 +109,15 @@ simulate env | actor ∷ rest | valid ∷ restValid | Spawn {NewIS} {B} act ⟶ ; blocked = blocked env ; store = newStore ; env-inboxes = [] ∷ env-inboxes env - ; actors-valid = newActValid ∷ valid' ∷ ∀map (valid-actor-suc (name-is-fresh env)) restValid - ; blocked-valid = ∀map (valid-actor-suc (name-is-fresh env)) (blocked-valid env) - ; messages-valid = [] ∷ map-suc (store env) (messages-valid env) (name-is-fresh env) - ; fresh-name = suc (fresh-name env) - ; name-is-fresh = newIsFresh + ; 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 → ∀ {n} → NameFresh store n → InboxesValid (inbox# n [ NewIS ] ∷ store) inbs - map-suc store [] frsh = [] - map-suc store (x ∷ valid) frsh = messages-valid-suc frsh x ∷ map-suc store valid frsh + 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 @@ -187,8 +186,7 @@ simulate env | actor ∷ rest | valid ∷ restValid | Receive ⟶ cont = keep-si ∷ restValid ; blocked-valid = blocked-valid env ; messages-valid = inboxes-valid inboxesAfter - ; fresh-name = fresh-name env - ; name-is-fresh = name-is-fresh env + ; name-supply = env .name-supply } simulate env | actor ∷ rest | valid ∷ restValid | SelectiveReceive filter ⟶ cont = keep-simulating (Selective (name actor) (receiveKind selectedMessage)) (env' selectedMessage) where @@ -230,8 +228,7 @@ simulate env | actor ∷ rest | valid ∷ restValid | SelectiveReceive filter }) ∷ restValid ; blocked-valid = blocked-valid env ; messages-valid = inboxes-valid inboxesAfter - ; fresh-name = fresh-name env - ; name-is-fresh = name-is-fresh env + ; name-supply = env .name-supply } simulate env | actor ∷ rest | valid ∷ restValid | Self ⟶ cont = keep-simulating (Self (name actor)) env' where diff --git a/src/Selective/SimulationEnvironment.agda b/src/Selective/SimulationEnvironment.agda index e8a1d20..5a8d1e7 100644 --- a/src/Selective/SimulationEnvironment.agda +++ b/src/Selective/SimulationEnvironment.agda @@ -5,11 +5,12 @@ open import Selective.ActorMonad open import Data.List using (List ; _∷_ ; [] ; map) open import Data.List.All using (All ; _∷_ ; [] ; lookup) renaming (map to ∀map) open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) -open import Data.Nat 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 Level using (Lift ; lift) -open import Size using (Size ; ∞) +open import Size using (Size ; Size<_ ; ↑_ ; ∞) open import Data.Empty using (⊥) open import Relation.Nullary using (Dec ; yes ; no ; ¬_) @@ -202,6 +203,72 @@ 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¬≡ 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 ] + +open NameSupply + +record NameSupplyStream (i : Size) (store : Store) : Set₁ where + coinductive + field + supply : NameSupply store + next : (IS : InboxShape) → {j : Size< i} → NameSupplyStream j (inbox# supply .name [ IS ] ∷ store) + + +-- helps show that all the names in the store are still valid if we add a new name on top, +-- if the new name is > than all the names already in the store. +suc-helper : ∀ {store name IS n} → + name ↦ IS ∈e store → + All (λ v → suc (NamedInbox.name v) Data.Nat.≤ n) store → + ¬[ 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 pr [p: actual-has-pointer ][handles: actual-handles-wanted ] = [p: (suc {pr = pr} actual-has-pointer) ][handles: actual-handles-wanted ] + +open NameSupplyStream + +next-name-supply : {store : Store} → (ns : NameSupply store) → (IS : InboxShape) → NameSupply (inbox# (ns .name) [ IS ] ∷ store) +next-name-supply ns IS = record { + name = suc (ns .name) + ; freshness-carrier = next-fresh + ; name-is-fresh = λ p → suc-helper p next-fresh + } + where + next-fresh = (s≤s (≤-reflexive refl)) ∷ ∀map ≤-step (ns .freshness-carrier) + +name-supply-singleton : {i : Size} → NameSupplyStream i [] +name-supply-singleton .supply = record { + name = 0 + ; freshness-carrier = [] + ; name-is-fresh = λ { () } + } +name-supply-singleton .next = stream-builder (name-supply-singleton .supply) + where + stream-builder : {i : Size} → {store : Store} → (ns : NameSupply store) → (IS : InboxShape) → {j : Size< i} → NameSupplyStream j (inbox# (ns .name) [ IS ] ∷ store) + stream-builder ns IS .supply = next-name-supply ns IS + stream-builder ns IS .next = stream-builder (next-name-supply ns IS) + -- 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 @@ -220,10 +287,7 @@ record Env : Set₂ where actors-valid : All (ValidActor store) acts blocked-valid : All (ValidActor store) blocked messages-valid : InboxesValid store env-inboxes - -- In each environment we keep track of the next fresh name, - -- and a proof that the name is not already used in the store. - fresh-name : Name - name-is-fresh : NameFresh store fresh-name + name-supply : NameSupplyStream ∞ store -- The empty environment empty-env : Env @@ -232,11 +296,10 @@ empty-env = record ; blocked = [] ; env-inboxes = [] ; store = [] - ; fresh-name = 0 ; actors-valid = [] ; blocked-valid = [] ; messages-valid = [] - ; name-is-fresh = [] + ; name-supply = name-supply-singleton } -- An environment containing a single actor. @@ -251,14 +314,13 @@ singleton-env {IS} {A} {post} actor = record ; pre-eq-refs = refl ; post = post ; computation = record { act = actor ; cont = [] } - ; name = 0 + ; name = name-supply-singleton .supply .name } ∷ [] ; blocked = [] ; env-inboxes = [] ∷ [] ; store = inbox# 0 [ IS ] ∷ [] - ; fresh-name = 1 ; actors-valid = (record { actor-has-inbox = zero ; references-have-pointer = [] }) ∷ [] ; blocked-valid = [] ; messages-valid = [] ∷ [] - ; name-is-fresh = Data.Nat.s≤s Data.Nat.z≤n ∷ [] + ; name-supply = name-supply-singleton .next IS } diff --git a/src/Simulate.agda b/src/Simulate.agda index f903213..d09642f 100644 --- a/src/Simulate.agda +++ b/src/Simulate.agda @@ -52,6 +52,8 @@ 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. @@ -82,25 +84,23 @@ simulate env | actor ∷ rest | valid ∷ restValid | (m ∞>>= f) ⟶ cont = ke 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) (fresh-name env)) env' +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# (fresh-name env) [ NewIS ] + newStoreEntry = inbox# (env .name-supply .supply .name) [ NewIS ] newStore : Store newStore = newStoreEntry ∷ store env newAct : Actor - newAct = new-actor act (fresh-name env) + newAct = new-actor act (env .name-supply .supply .name) newActValid : ValidActor newStore newAct newActValid = record { actor-has-inbox = zero ; references-have-pointer = [] } - newIsFresh : NameFresh newStore (suc (fresh-name env)) - newIsFresh = s≤s (≤-reflexive refl) ∷ ∀map ≤-step (name-is-fresh env) actor' : Actor actor' = add-reference actor newStoreEntry (Return _ ⟶ cont) valid' : ValidActor newStore actor' valid' = record { - actor-has-inbox = suc {pr = suc-helper (actor-has-inbox valid) (name-is-fresh env)} (actor-has-inbox valid) + 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 (suc-helper (actual-has-pointer p) (name-is-fresh env)) p) + (λ p → suc-p (env .name-supply .supply .name-is-fresh (actual-has-pointer p)) p) (references-have-pointer valid) } env' : Env env' = record @@ -108,16 +108,15 @@ simulate env | actor ∷ rest | valid ∷ restValid | Spawn {NewIS} {B} act ⟶ ; blocked = blocked env ; store = newStore ; env-inboxes = [] ∷ env-inboxes env - ; actors-valid = newActValid ∷ valid' ∷ ∀map (valid-actor-suc (name-is-fresh env)) restValid - ; blocked-valid = ∀map (valid-actor-suc (name-is-fresh env)) (blocked-valid env) - ; messages-valid = [] ∷ map-suc (store env) (messages-valid env) (name-is-fresh env) - ; fresh-name = suc (fresh-name env) - ; name-is-fresh = newIsFresh + ; 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 → ∀ {n} → NameFresh store n → InboxesValid (inbox# n [ NewIS ] ∷ store) inbs - map-suc store [] frsh = [] - map-suc store (x ∷ valid) frsh = messages-valid-suc frsh x ∷ map-suc store valid frsh + 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 @@ -186,8 +185,7 @@ simulate env | actor ∷ rest | valid ∷ restValid | Receive ⟶ cont = keep-si ∷ restValid ; blocked-valid = blocked-valid env ; messages-valid = inboxes-valid inboxesAfter - ; fresh-name = fresh-name env - ; name-is-fresh = name-is-fresh env + ; name-supply = env .name-supply } simulate env | actor ∷ rest | valid ∷ restValid | Self ⟶ cont = keep-simulating (Self (name actor)) env' where diff --git a/src/SimulationEnvironment.agda b/src/SimulationEnvironment.agda index 5551ee0..e96f3d8 100644 --- a/src/SimulationEnvironment.agda +++ b/src/SimulationEnvironment.agda @@ -5,11 +5,12 @@ open import ActorMonad open import Data.List using (List ; _∷_ ; [] ; map) open import Data.List.All using (All ; _∷_ ; [] ; lookup) renaming (map to ∀map) open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) -open import Data.Nat 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 Level using (Lift ; lift) -open import Size using (Size ; ∞) +open import Size using (Size ; Size<_ ; ↑_ ; ∞) open import Data.Empty using (⊥) open import Relation.Nullary using (Dec ; yes ; no ; ¬_) @@ -199,6 +200,72 @@ 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¬≡ 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 ] + +open NameSupply + +record NameSupplyStream (i : Size) (store : Store) : Set₁ where + coinductive + field + supply : NameSupply store + next : (IS : InboxShape) → {j : Size< i} → NameSupplyStream j (inbox# supply .name [ IS ] ∷ store) + + +-- helps show that all the names in the store are still valid if we add a new name on top, +-- if the new name is > than all the names already in the store. +suc-helper : ∀ {store name IS n} → + name ↦ IS ∈e store → + All (λ v → suc (NamedInbox.name v) Data.Nat.≤ n) store → + ¬[ 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 pr [p: actual-has-pointer ][handles: actual-handles-wanted ] = [p: (suc {pr = pr} actual-has-pointer) ][handles: actual-handles-wanted ] + +open NameSupplyStream + +next-name-supply : {store : Store} → (ns : NameSupply store) → (IS : InboxShape) → NameSupply (inbox# (ns .name) [ IS ] ∷ store) +next-name-supply ns IS = record { + name = suc (ns .name) + ; freshness-carrier = next-fresh + ; name-is-fresh = λ p → suc-helper p next-fresh + } + where + next-fresh = (s≤s (≤-reflexive refl)) ∷ ∀map ≤-step (ns .freshness-carrier) + +name-supply-singleton : {i : Size} → NameSupplyStream i [] +name-supply-singleton .supply = record { + name = 0 + ; freshness-carrier = [] + ; name-is-fresh = λ { () } + } +name-supply-singleton .next = stream-builder (name-supply-singleton .supply) + where + stream-builder : {i : Size} → {store : Store} → (ns : NameSupply store) → (IS : InboxShape) → {j : Size< i} → NameSupplyStream j (inbox# (ns .name) [ IS ] ∷ store) + stream-builder ns IS .supply = next-name-supply ns IS + stream-builder ns IS .next = stream-builder (next-name-supply ns IS) + -- 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 @@ -217,10 +284,7 @@ record Env : Set₂ where actors-valid : All (ValidActor store) acts blocked-valid : All (ValidActor store) blocked messages-valid : InboxesValid store env-inboxes - -- In each environment we keep track of the next fresh name, - -- and a proof that the name is not already used in the store. - fresh-name : Name - name-is-fresh : NameFresh store fresh-name + name-supply : NameSupplyStream ∞ store -- The empty environment empty-env : Env @@ -229,11 +293,10 @@ empty-env = record ; blocked = [] ; env-inboxes = [] ; store = [] - ; fresh-name = 0 ; actors-valid = [] ; blocked-valid = [] ; messages-valid = [] - ; name-is-fresh = [] + ; name-supply = name-supply-singleton } -- An environment containing a single actor. @@ -248,14 +311,13 @@ singleton-env {IS} {A} {post} actor = record ; pre-eq-refs = refl ; post = post ; computation = record { act = actor ; cont = [] } - ; name = 0 + ; name = name-supply-singleton .supply .name } ∷ [] ; blocked = [] ; env-inboxes = [] ∷ [] ; store = inbox# 0 [ IS ] ∷ [] - ; fresh-name = 1 ; actors-valid = (record { actor-has-inbox = zero ; references-have-pointer = [] }) ∷ [] ; blocked-valid = [] ; messages-valid = [] ∷ [] - ; name-is-fresh = Data.Nat.s≤s Data.Nat.z≤n ∷ [] + ; name-supply = name-supply-singleton .next IS }