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")
|
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")
|
2015-03-05 14:54:12 +00:00
|
|
|
|
|
|
|
(provide (struct-out external-event)
|
|
|
|
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
|
2015-03-05 14:54:12 +00:00
|
|
|
run-ground)
|
|
|
|
|
|
|
|
;;---------------------------------------------------------------------------
|
|
|
|
;; 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.
|
|
|
|
(define (send-ground-message body)
|
|
|
|
(async-channel-put (current-ground-event-async-channel) (message body)))
|
|
|
|
|
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.
|
|
|
|
(define (send-ground-patch p)
|
|
|
|
(async-channel-put (current-ground-event-async-channel) p))
|
|
|
|
|
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)))
|
|
|
|
|
|
|
|
;; Action* -> Void
|
2016-04-07 07:42:54 +00:00
|
|
|
;; Runs a ground VM, booting the outermost Dataspace with the given Actions.
|
2015-03-05 14:54:12 +00:00
|
|
|
(define (run-ground . boot-actions)
|
|
|
|
(let await-interrupt ((inert? #f)
|
2016-04-07 07:42:54 +00:00
|
|
|
(w (make-dataspace boot-actions))
|
2016-03-12 16:54:31 +00:00
|
|
|
(interests trie-empty))
|
2016-01-22 02:55:41 +00:00
|
|
|
;; (log-info "GROUND INTERESTS:\n~a" (trie->pretty-string interests))
|
|
|
|
(if (and inert? (trie-empty? interests))
|
2015-03-05 14:54:12 +00:00
|
|
|
(begin (log-info "run-ground: Terminating because inert")
|
|
|
|
(void))
|
|
|
|
(let ((e (apply sync
|
|
|
|
(current-ground-event-async-channel)
|
|
|
|
(if inert? never-evt idle-handler)
|
|
|
|
(extract-active-events interests))))
|
2016-04-07 07:42:54 +00:00
|
|
|
(trace-process-step e #f dataspace-handle-event w)
|
|
|
|
(define resulting-transition (clean-transition (dataspace-handle-event e w)))
|
|
|
|
(trace-process-step-result e #f dataspace-handle-event w #f resulting-transition)
|
2015-03-21 21:30:48 +00:00
|
|
|
(match resulting-transition
|
2015-03-05 14:54:12 +00:00
|
|
|
[#f ;; inert
|
|
|
|
(await-interrupt #t w interests)]
|
|
|
|
[(transition w actions)
|
|
|
|
(let process-actions ((actions actions) (interests interests))
|
|
|
|
(match actions
|
|
|
|
['() (await-interrupt #f w interests)]
|
|
|
|
[(cons a actions)
|
|
|
|
(match a
|
|
|
|
[(? patch? p)
|
2015-06-20 00:29:16 +00:00
|
|
|
(process-actions actions (apply-patch interests (label-patch p (datum-tset 'root))))]
|
2015-03-05 14:54:12 +00:00
|
|
|
[_
|
|
|
|
(log-warning "run-ground: ignoring useless meta-action ~v" a)
|
|
|
|
(process-actions actions interests)])]))])))))
|