diff --git a/racket/typed/examples/roles/flink.rkt b/racket/typed/examples/roles/flink.rkt index 777d494..f71b164 100644 --- a/racket/typed/examples/roles/flink.rkt +++ b/racket/typed/examples/roles/flink.rkt @@ -112,6 +112,19 @@ JobManager and the TaskManager, and one between the TaskManager and its TaskRunners. |# +(define-type-alias TaskAssigner + (Role (assign) + (Shares (TaskAssignment ID ID ConcreteTask)) + ;; would be nice to say how the IDs relate to each other (first two are the same) + (Reacts (Know (TaskState ID ID ID ★/t)) + (Branch (Stop assign) + (Effs))))) + +(define-type-alias TaskPerformer + (Role (listen) + (During (TaskAssignment ID ID ConcreteTask) + (Shares (TaskState ID ID TaskID TaskStateDesc))))) + #| Job Submission Protocol ----------------------- @@ -389,11 +402,11 @@ The JobManager then performs the job and, when finished, asserts (job-finished I ;; ID -> ... (define (assign-task [mngr : ID]) - (start-facet this-facet + (start-facet assign (assert (task-assignment mngr job-id t)) (on (retracted (task-manager mngr discard)) ;; our task manager has crashed - (stop this-facet + (stop assign (set! task-mngr not-a-real-task-manager))) (on start ;; N.B. when this line was here, and not after `(when mngr ...)` above, @@ -413,14 +426,14 @@ The JobManager then performs the job and, when finished, asserts (job-finished I ;; don't think we need a release-slot! here, because if we've heard back from a task manager, ;; they should have told us a different slot count since we tried to give them work (log "JM overloaded manager ~a with task ~a" mngr this-id) - (stop this-facet + (stop assign (set! task-mngr not-a-real-task-manager))] [(finished $results) (log "JM receives the results of task ~a" this-id) (stop perform (k this-id results))])))) (define (select-a-task-manager) - (start-facet this-facet + (start-facet select (begin/dataflow (when (equal? (ref task-mngr) not-a-real-task-manager) (define mngr? diff --git a/racket/typed/proto.rkt b/racket/typed/proto.rkt index 5a98560..7f2efa5 100644 --- a/racket/typed/proto.rkt +++ b/racket/typed/proto.rkt @@ -1041,11 +1041,7 @@ (esc #f)) (define assertions1 (hash-ref assertion#1 sn1)) (define assertions2 (hash-ref assertion#2 sn2)) - (define superset? - (for/and ([assertion2 (in-set assertions2)]) - (for/or ([assertion1 (in-set assertions1)]) - (<:? assertion1 assertion2)))) - (unless superset? + (unless (assertion-superset? assertions1 assertions2) (return #f)) (define transitions1 (state-transitions (hash-ref st#1 sn1))) (define transitions2 (state-transitions (hash-ref st#2 sn2))) @@ -1085,7 +1081,7 @@ (for/and ([goal (in-set matching)]) (define hypotheses (set-remove matching goal)) (verify goal (set-union hypotheses assumptions))))]))) - (verify (equiv st0-1 st0-2) (set))) + (verify (equiv st0-1 st0-2) (set))) ;; (Sequenceof StateName) Role -> (Hashof StateName (Setof τ)) ;; map each state name to its active assertions @@ -1105,6 +1101,13 @@ (values (Role-nm role) (role-assertions role)))) +;; (Setof τ) (Setof τ) -> Bool +;; is as1 a superset of as2? +(define (assertion-superset? as1 as2) + (for/and ([assertion2 (in-set as2)]) + (for/or ([assertion1 (in-set as1)]) + (<:? assertion2 assertion1)))) + (module+ test (test-case "simplest simul" @@ -1350,16 +1353,18 @@ (Branch (Effs (Stop get-quotes)) (Effs))))))) (test-case "parsed types are (not) the same as my manual conversions" - ;; because I parse (Bind τ) as ⋆, whereas my manual conversions use τ - (check-false (simulates? (parse-T real-seller-ty) seller-actual)) + ;; because I parse (Bind τ) as ⋆, whereas my manual conversions use τ thus + ;; the "real" types are more specialized and implement the manual + ;; conversions, but not vice versa + (check-true (simulates? (parse-T real-seller-ty) seller-actual)) (check-false (simulates? seller-actual (parse-T real-seller-ty))) - (check-false (simulates? (parse-T real-member-ty) member-actual)) + (check-true (simulates? (parse-T real-member-ty) member-actual)) (check-false (simulates? member-actual (parse-T real-member-ty))) - (check-false (simulates? (parse-T real-leader-ty) leader-actual)) + (check-true (simulates? (parse-T real-leader-ty) leader-actual)) (check-false (simulates? leader-actual (parse-T real-leader-ty))) - (check-false (simulates? (parse-T real-leader-ty) leader-revised)) + (check-true (simulates? (parse-T real-leader-ty) leader-revised)) (check-false (simulates? leader-revised (parse-T real-leader-ty))))) (define real-seller-ty @@ -1501,3 +1506,80 @@ (define jm (compile jmr)) (check-true (role-graph? jm)) (check-true (simulates? jmr jmr)))) + +(define task-performer-spec + '(Role + (listen) + (Reacts + (Know + (TaskAssignment + Symbol + Symbol + (Task + Int + (U + (MapWork String) + (ReduceWork (Hash String Int) (Hash String Int)))))) + (Role + (during-inner) + (Reacts + (¬Know + (TaskAssignment + Symbol + Symbol + (Task + Int + (U + (MapWork String) + (ReduceWork (Hash String Int) (Hash String Int)))))) + (Stop during-inner)) + (Shares + (TaskState + Symbol + Symbol + Int + (U (Finished (Hash String Int)) Symbol))))))) + +(module+ test + (test-case "parse and compile task-performer-spec" + (check-true (Role? (parse-T task-performer-spec))) + (check-true (role-graph? (compile (parse-T task-performer-spec)))))) + +(define task-runner-ty + '(Role + (runner) + (Shares (TaskRunner Symbol (U (Executing Int) Symbol))) + (Reacts + (Know + (TaskAssignment + Symbol + (Bind Symbol) + (Task + (Bind Int) + (Bind + (U + (MapWork String) + (ReduceWork (Hash String Int) (Hash String Int))))))) + (Role + (during-inner) + (Shares + (TaskState Symbol Symbol Int (U (Finished (Hash String Int)) Symbol))) + (Reacts + (¬Know + (TaskAssignment + Symbol + Symbol + (Task + Int + (U + (MapWork String) + (ReduceWork (Hash String Int) (Hash String Int)))))) + (Stop during-inner)))) + (Reacts OnDataflow))) + +(module+ test + (test-case "parse and compile task-runner-ty" + (check-true (Role? (parse-T task-runner-ty))) + (check-true (role-graph? (compile (parse-T task-runner-ty)))) + (check-true (simulates? (parse-T task-runner-ty) + (parse-T task-performer-spec)))))