2015-03-05 14:54:12 +00:00
|
|
|
#lang racket/base
|
2016-04-07 07:42:54 +00:00
|
|
|
;; Breaking the infinite tower of nested Dataspaces, connecting to the "real world" at the fracture line.
|
2015-03-05 14:54:12 +00:00
|
|
|
|
|
|
|
(require racket/async-channel)
|
|
|
|
(require racket/set)
|
|
|
|
(require racket/match)
|
|
|
|
(require racket/list)
|
|
|
|
(require "core.rkt")
|
2016-07-30 17:02:07 +00:00
|
|
|
(require "dataspace.rkt")
|
2016-07-20 23:27:40 +00:00
|
|
|
(require "hierarchy.rkt")
|
2015-03-21 21:30:48 +00:00
|
|
|
(require "trace.rkt")
|
2015-03-05 14:54:12 +00:00
|
|
|
(require "trace/stderr.rkt")
|
2015-06-20 00:29:16 +00:00
|
|
|
(require "tset.rkt")
|
2016-07-30 17:02:07 +00:00
|
|
|
(require "protocol/standard-relay.rkt")
|
2017-03-08 22:59:55 +00:00
|
|
|
(require "trie.rkt")
|
2015-03-05 14:54:12 +00:00
|
|
|
|
|
|
|
(provide (struct-out external-event)
|
2016-08-31 18:11:16 +00:00
|
|
|
current-ground-event-async-channel
|
2015-03-05 14:54:12 +00:00
|
|
|
send-ground-message
|
Switch from timer-expired /messages/ to /assertions/ at ground level.
Previously, the timer driver caused the background thread to call
send-ground-message to indicate that a timer had expired. However,
this can lead to a race! In cases where a timer expires very soon, the
channel-put of the set-timer instruction leads shortly thereafter to a
send-ground-message which then races the establishment of the
metalevel-1 subscription to the timer-expired events that are coming
from the background thread.
The race cannot occur in the sequential implementation because the
network makes sure to enqueue the transition actions resulting from
the set-timer message delivery ahead of any enqueueing of the
timer-expired ground message, so that by the time the ground message
is processed, the relevant subscription always exists.
In a looser implementation, however, this level of synchronised
activity may not exist, and the ground message may overtake the
subscription establishment.
Therefore, I've changed the driver to instead use ground /assertions/
to signal expired timers. Upon processing of such an assertion, the
driver cleans it up. This is very similar to hardware interrupts,
where the driver has to "clear the interrupt" in order to let the
system continue properly.
2016-01-21 22:38:12 +00:00
|
|
|
send-ground-patch
|
2016-07-21 02:13:43 +00:00
|
|
|
send-ground-event
|
|
|
|
signal-background-activity!
|
2015-03-05 14:54:12 +00:00
|
|
|
run-ground)
|
|
|
|
|
2016-11-20 22:46:31 +00:00
|
|
|
(define-logger syndicate/ground)
|
|
|
|
|
2015-03-05 14:54:12 +00:00
|
|
|
;;---------------------------------------------------------------------------
|
|
|
|
;; Communication via regular subscription and messages from other threads
|
|
|
|
|
|
|
|
;; (Parameterof (Option AsyncChannel))
|
|
|
|
;; Communication channel from auxiliary (usually driver) threads to
|
|
|
|
;; the currently-active ground VM.
|
|
|
|
(define current-ground-event-async-channel (make-parameter (make-async-channel)))
|
|
|
|
|
|
|
|
;; Any -> Void
|
|
|
|
;; Sends a message at the ground-VM metalevel.
|
2016-07-20 23:27:40 +00:00
|
|
|
(define (send-ground-message body #:path [path '()])
|
|
|
|
(async-channel-put (current-ground-event-async-channel) (target-event path (message body))))
|
2015-03-05 14:54:12 +00:00
|
|
|
|
Switch from timer-expired /messages/ to /assertions/ at ground level.
Previously, the timer driver caused the background thread to call
send-ground-message to indicate that a timer had expired. However,
this can lead to a race! In cases where a timer expires very soon, the
channel-put of the set-timer instruction leads shortly thereafter to a
send-ground-message which then races the establishment of the
metalevel-1 subscription to the timer-expired events that are coming
from the background thread.
The race cannot occur in the sequential implementation because the
network makes sure to enqueue the transition actions resulting from
the set-timer message delivery ahead of any enqueueing of the
timer-expired ground message, so that by the time the ground message
is processed, the relevant subscription always exists.
In a looser implementation, however, this level of synchronised
activity may not exist, and the ground message may overtake the
subscription establishment.
Therefore, I've changed the driver to instead use ground /assertions/
to signal expired timers. Upon processing of such an assertion, the
driver cleans it up. This is very similar to hardware interrupts,
where the driver has to "clear the interrupt" in order to let the
system continue properly.
2016-01-21 22:38:12 +00:00
|
|
|
;; Patch -> Void
|
|
|
|
;; Injects a patch into the ground-VM metalevel. It will appear to be
|
|
|
|
;; asserted by the environment in general. The obligation is on the caller
|
|
|
|
;; to ensure that patches do not interfere between drivers.
|
2016-07-20 23:27:40 +00:00
|
|
|
(define (send-ground-patch p #:path [path '()])
|
|
|
|
(async-channel-put (current-ground-event-async-channel) (target-event path p)))
|
Switch from timer-expired /messages/ to /assertions/ at ground level.
Previously, the timer driver caused the background thread to call
send-ground-message to indicate that a timer had expired. However,
this can lead to a race! In cases where a timer expires very soon, the
channel-put of the set-timer instruction leads shortly thereafter to a
send-ground-message which then races the establishment of the
metalevel-1 subscription to the timer-expired events that are coming
from the background thread.
The race cannot occur in the sequential implementation because the
network makes sure to enqueue the transition actions resulting from
the set-timer message delivery ahead of any enqueueing of the
timer-expired ground message, so that by the time the ground message
is processed, the relevant subscription always exists.
In a looser implementation, however, this level of synchronised
activity may not exist, and the ground message may overtake the
subscription establishment.
Therefore, I've changed the driver to instead use ground /assertions/
to signal expired timers. Upon processing of such an assertion, the
driver cleans it up. This is very similar to hardware interrupts,
where the driver has to "clear the interrupt" in order to let the
system continue properly.
2016-01-21 22:38:12 +00:00
|
|
|
|
2016-07-21 02:13:43 +00:00
|
|
|
;; Event -> Void
|
|
|
|
(define (send-ground-event e #:path [path '()])
|
|
|
|
(async-channel-put (current-ground-event-async-channel) (target-event path e)))
|
|
|
|
|
|
|
|
;;---------------------------------------------------------------------------
|
|
|
|
|
|
|
|
(struct background-activity-signal (delta) #:prefab)
|
|
|
|
|
|
|
|
(define (signal-background-activity! active?)
|
|
|
|
(async-channel-put (current-ground-event-async-channel)
|
|
|
|
(background-activity-signal (if active? 1 -1))))
|
|
|
|
|
2015-03-05 14:54:12 +00:00
|
|
|
;;---------------------------------------------------------------------------
|
|
|
|
;; Communication via RacketEvents
|
|
|
|
|
|
|
|
;; A GroundEvent is a pair of a Racket (evt?) event and its yielded
|
|
|
|
;; results.
|
|
|
|
;; - (external-event RacketEvent (Listof Any))
|
|
|
|
(struct external-event (descriptor values) #:prefab)
|
|
|
|
|
|
|
|
;; RacketEvent -> RacketEvent
|
|
|
|
;; Wraps a CML-style Racket event with a handler that sends the event
|
|
|
|
;; results via the ground VM.
|
|
|
|
(define (event-handler descriptor)
|
|
|
|
(handle-evt descriptor (lambda vs (message (external-event descriptor vs)))))
|
|
|
|
|
|
|
|
;; Projection
|
|
|
|
;; Used to extract event descriptors and results from subscriptions
|
2016-04-07 07:42:54 +00:00
|
|
|
;; from the ground VM's contained Dataspace.
|
2016-03-12 16:54:31 +00:00
|
|
|
(define event-projection (observe (external-event (?!) ?)))
|
2015-03-05 14:54:12 +00:00
|
|
|
|
|
|
|
;; Interests -> (Listof RacketEvent)
|
|
|
|
;; Projects out the active event subscriptions from the given interests.
|
|
|
|
(define (extract-active-events interests)
|
2016-01-22 02:55:41 +00:00
|
|
|
(define es (trie-project/set/single interests event-projection))
|
2015-03-05 14:54:12 +00:00
|
|
|
;; TODO: how should the following error be handled, ideally?
|
|
|
|
;; In principle, security restrictions should make it impossible.
|
|
|
|
;; But absent those, what should be done? Should an offending
|
|
|
|
;; process be identified and terminated?
|
|
|
|
(unless es (error 'extract-active-events "User program subscribed to wildcard event"))
|
|
|
|
(for/list [(e (in-set es))] (event-handler e)))
|
|
|
|
|
|
|
|
;;---------------------------------------------------------------------------
|
|
|
|
|
|
|
|
;; RacketEvent
|
|
|
|
;; Used only when the system is not provably inert, in order to let it
|
|
|
|
;; take further internal reductions.
|
|
|
|
(define idle-handler
|
|
|
|
(handle-evt (system-idle-evt) (lambda _ #f)))
|
|
|
|
|
2016-07-21 02:13:43 +00:00
|
|
|
;; RacketEvent
|
|
|
|
;; Used only when the system is locally not inert, but background
|
|
|
|
;; activity is continuing.
|
|
|
|
(define poll-handler
|
|
|
|
(handle-evt always-evt (lambda _ #f)))
|
|
|
|
|
2017-02-28 23:43:19 +00:00
|
|
|
;; Boolean Process AssertionSet Natural -> AssertionSet
|
|
|
|
;; Returns the final set of active assertions at groundmost level.
|
2016-07-30 17:36:03 +00:00
|
|
|
(define (await-interrupt inert? proc interests background-activity-count)
|
2016-07-30 17:02:07 +00:00
|
|
|
;; (log-info "~a ~a GROUND INTERESTS:\n~a"
|
|
|
|
;; inert?
|
|
|
|
;; background-activity-count
|
|
|
|
;; (trie->pretty-string interests))
|
2017-02-28 23:43:19 +00:00
|
|
|
(define active-events (extract-active-events interests))
|
2017-03-08 22:59:55 +00:00
|
|
|
;; use the presence of subscriptions to indicate whether the program is
|
|
|
|
;; waiting on a driver
|
|
|
|
(define ground-subscriptions (trie-step interests observe-parenthesis))
|
|
|
|
(if (and inert? (zero? background-activity-count) (trie-empty? ground-subscriptions))
|
2016-11-20 22:46:31 +00:00
|
|
|
(begin (log-syndicate/ground-debug "run-ground: Terminating because inert")
|
2017-02-28 23:43:19 +00:00
|
|
|
interests)
|
2016-07-30 17:02:07 +00:00
|
|
|
(match (apply sync
|
|
|
|
(current-ground-event-async-channel)
|
|
|
|
(cond
|
|
|
|
[inert? never-evt]
|
|
|
|
[(zero? background-activity-count) idle-handler]
|
|
|
|
[else poll-handler])
|
2017-02-28 23:43:19 +00:00
|
|
|
active-events)
|
2016-07-30 17:02:07 +00:00
|
|
|
[(background-activity-signal delta)
|
|
|
|
;; (log-info "background-activity-count ~v" (+ background-activity-count delta))
|
2016-07-30 17:36:03 +00:00
|
|
|
(await-interrupt inert? proc interests (+ background-activity-count delta))]
|
2016-07-30 17:02:07 +00:00
|
|
|
[e
|
2016-07-30 17:36:03 +00:00
|
|
|
(inject-event e proc interests background-activity-count)])))
|
|
|
|
|
2017-02-28 23:43:19 +00:00
|
|
|
;; Event Process AssertionSet Natural -> AssertionSet
|
|
|
|
;; Returns the final set of active assertions at groundmost level.
|
2016-07-30 17:36:03 +00:00
|
|
|
(define (inject-event e proc interests background-activity-count)
|
2016-08-25 17:07:27 +00:00
|
|
|
(trace-event-consumed #f e)
|
|
|
|
(trace-turn-begin #f proc)
|
2016-07-30 17:36:03 +00:00
|
|
|
(define resulting-transition (clean-transition ((process-behavior proc) e (process-state proc))))
|
|
|
|
(process-transition resulting-transition proc interests background-activity-count))
|
|
|
|
|
2017-02-28 23:43:19 +00:00
|
|
|
;; (Listof Action) AssertionSet -> AssertionSet
|
|
|
|
;; Incorporates patches into the given assertion set.
|
|
|
|
(define (process-actions actions interests)
|
|
|
|
(match actions
|
|
|
|
['() interests]
|
|
|
|
[(cons a actions)
|
|
|
|
(match a
|
|
|
|
[(? patch? p)
|
|
|
|
(process-actions actions (apply-patch interests (label-patch p (datum-tset 'root))))]
|
|
|
|
[_
|
|
|
|
(log-syndicate/ground-warning "run-ground: ignoring useless meta-action ~v" a)
|
|
|
|
(process-actions actions interests)])]))
|
|
|
|
|
|
|
|
;; Transition Process AssertionSet Natural -> AssertionSet
|
|
|
|
;; Returns the final set of active assertions at groundmost level.
|
2016-07-30 17:36:03 +00:00
|
|
|
(define (process-transition resulting-transition proc interests background-activity-count)
|
2016-07-30 17:02:07 +00:00
|
|
|
(match resulting-transition
|
|
|
|
[#f ;; inert
|
2016-08-25 17:07:27 +00:00
|
|
|
(trace-turn-end #f proc)
|
2016-07-30 17:36:03 +00:00
|
|
|
(await-interrupt #t proc interests background-activity-count)]
|
2017-02-28 23:43:19 +00:00
|
|
|
[(<quit> exn actions)
|
2016-08-25 17:07:27 +00:00
|
|
|
(trace-turn-end #f proc)
|
|
|
|
(trace-actor-exit #f exn)
|
2016-11-20 22:46:31 +00:00
|
|
|
(log-syndicate/ground-debug "run-ground: Terminating by request")
|
2017-02-28 23:43:19 +00:00
|
|
|
(process-actions actions interests)]
|
2016-07-30 17:36:03 +00:00
|
|
|
[(transition new-state actions)
|
2016-08-25 17:07:27 +00:00
|
|
|
(trace-turn-end #f (process (process-name proc) (process-behavior proc) new-state))
|
2017-02-28 23:43:19 +00:00
|
|
|
(let ((proc (update-process-state proc new-state))
|
|
|
|
(new-interests (process-actions actions interests)))
|
|
|
|
(await-interrupt #f proc new-interests background-activity-count))]))
|
|
|
|
|
|
|
|
;; Action* -> AssertionSet
|
2016-04-07 07:42:54 +00:00
|
|
|
;; Runs a ground VM, booting the outermost Dataspace with the given Actions.
|
2017-02-28 23:43:19 +00:00
|
|
|
;; Returns the final set of active assertions at groundmost level.
|
2015-03-05 14:54:12 +00:00
|
|
|
(define (run-ground . boot-actions)
|
2017-02-25 16:16:25 +00:00
|
|
|
(run-ground* (dataspace-actor #:name 'ground boot-actions)))
|
2016-07-30 17:02:07 +00:00
|
|
|
|
2017-02-28 23:43:19 +00:00
|
|
|
;; actor -> AssertionSet
|
|
|
|
;; Returns the final set of active assertions at groundmost level.
|
2016-07-30 17:02:07 +00:00
|
|
|
(define (run-ground* s)
|
2017-02-15 23:18:19 +00:00
|
|
|
(define-values (proc t) (actor->process+transition s))
|
2016-07-30 17:48:42 +00:00
|
|
|
(process-transition t proc trie-empty 0))
|