Ensure (??) that relays' assertions can't outlive them

This commit is contained in:
Tony Garnock-Jones 2018-05-02 18:10:52 +01:00
parent dd123f4a27
commit 17cee51342
3 changed files with 93 additions and 15 deletions

View File

@ -455,7 +455,8 @@
(define ds (actor-dataspace ac))
(push-script! ac (lambda ()
(for [((eid ep) (in-hash (facet-endpoints f)))]
(destroy-endpoint! ds ac f ep)))))
(destroy-endpoint! ds ac f ep))
(hash-clear! (facet-endpoints f)))))
(define (abandon-queued-work! ac)
(set-actor-pending-actions! ac (make-queue))
@ -535,8 +536,8 @@
(when ep
(define ac (facet-actor f))
(define ds (actor-dataspace ac))
(hash-remove! eps eid)
(destroy-endpoint! ds ac f ep)))
(destroy-endpoint! ds ac f ep)
(hash-remove! eps eid)))
(define (destroy-endpoint! ds ac f ep)
(match-define (endpoint eid assertion handler _update-fn) ep)

View File

@ -106,12 +106,11 @@
;; (log-info "~a (cleanup) ~v" inner-actor term)
(adhoc-retract! inner-actor term))))
(schedule-inner!))))
(hash-set! inbound-endpoints
x
(add-endpoint! outer-facet
"dataspace-relay (observe (inbound ...))"
#t
(lambda () (values (observe x) i)))))))
(add-endpoint-if-live! outer-facet
inbound-endpoints
x
"dataspace-relay (observe (inbound ...))"
(lambda () (values (observe x) i))))))
(on (message (*quit-dataspace*))
(with-current-facet [outer-facet]
@ -128,12 +127,11 @@
;; (log-info "~a (asserted (outbound ~v))" inner-actor x)
(with-current-facet [outer-facet]
(with-non-script-context
(hash-set! outbound-endpoints
x
(add-endpoint! outer-facet
"dataspace-relay (outbound ...)"
#t
(lambda () (values x #f)))))))
(add-endpoint-if-live! outer-facet
outbound-endpoints
x
"dataspace-relay (outbound ...)"
(lambda () (values x #f))))))
(on (retracted (outbound $x))
;; (log-info "~a (retracted (outbound ~v))" inner-actor x)
@ -146,3 +144,23 @@
;; (log-info "~a (message (outbound ~v))" inner-actor x)
(with-current-facet [outer-facet]
(send! x))))
(define (add-endpoint-if-live! f table key desc update-fn)
(when (facet-live? f)
;;
;; ^ Check that `f` is still alive, because we're (carefully!!)
;; violating an invariant of `dataspace.rkt` by adding an endpoint
;; well after the construction of the facet we're in. We may be
;; executing this handler just after clean shutdown of the facet
;; by a `quit-dataspace!` request, and in that case we MUST NOT
;; add any further endpoints because their assertions will not get
;; removed, because cleanup (as part of `(quit)` processing) has
;; already been done.
;;
;; We don't have to do a similar check before calling
;; `remove-endpoint!`, because shortly after all (both) calls to
;; `destroy-endpoint!`, all destroyed endpoints are removed from
;; the `facet-endpoints` table, ensuring they won't be processed
;; again.
;;
(hash-set! table key (add-endpoint! f desc #t update-fn))))

View File

@ -0,0 +1,59 @@
#lang imperative-syndicate/test-implementation
;; Tests that adhoc assertions are always removed on termination, even
;; when being relayed across a dataspace boundary.
(require imperative-syndicate/bag)
(require imperative-syndicate/pattern)
(message-struct trigger ())
(define (spawn-seen-monitor)
(spawn #:name 'monitor
(on (asserted $x) (printf "Seen: ~v\n" x))))
(define (spawn-double-trigger)
;; Sending the trigger twice is one of the critical factors for this test case
(spawn* #:name 'double-trigger
(until (asserted (observe (trigger))))
(send! (trigger))
(send! (trigger))))
(define (only-seen-monitor-output?)
(expected-output "Seen: '#s(observe #s(capture #s(discard)))"))
(define (only-seen-monitor-assertions?)
(lambda ()
(define actual-assertions (dataspace-assertions (final-dataspace)))
(define expected-assertions (make-hash (list (cons (observe (capture (discard))) 1))))
(or (equal? actual-assertions expected-assertions)
(error 'only-seen-monitor-assertions? "Actual-assertions ~v <> expected-assertions ~v"
actual-assertions
expected-assertions))))
(test-case
[(spawn-seen-monitor)
(dataspace #:name 'middle-dataspace
(spawn-double-trigger)
(dataspace #:name 'inner-dataspace
(spawn #:name 'actor0
(on (message (inbound (trigger))) (quit-dataspace!))
(on (message (inbound (trigger)))
(flush!)
(assert! (outbound (outbound 'B)))))))]
no-crashes
(only-seen-monitor-output?)
(only-seen-monitor-assertions?))
(test-case
[(spawn-seen-monitor)
(dataspace #:name 'middle-dataspace
(spawn-double-trigger)
(dataspace #:name 'inner-dataspace
(spawn #:name 'actor0
(on (message (inbound (trigger))) (quit-dataspace!))
(on (message (inbound (trigger)))
(flush!)
(react (assert (outbound (outbound 'B))))))))]
no-crashes
(only-seen-monitor-output?)
(only-seen-monitor-assertions?))