From e9aaa45d9b6427d681d6cce087b2fddae900f7e2 Mon Sep 17 00:00:00 2001 From: Tony Garnock-Jones Date: Tue, 20 Mar 2012 11:33:54 -0400 Subject: [PATCH] WIP --- os2.rkt | 151 ++++++++++++++++++++++----- relation.rkt | 42 ++++++-- struct-map.rkt | 42 ++++++++ unify.rkt | 276 +++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 478 insertions(+), 33 deletions(-) create mode 100644 struct-map.rkt create mode 100644 unify.rkt diff --git a/os2.rkt b/os2.rkt index c410b40..4b6ddaa 100644 --- a/os2.rkt +++ b/os2.rkt @@ -2,6 +2,11 @@ ;; Virtualized operating system, this time with presence. (require racket/match) +(require "relation.rkt") +(require "unify.rkt") + +;; Endpoints are the units of deduplication. +;; Flows (in canonical form) are the units of presence. ;;--------------------------------------------------------------------------- ;; Data definitions @@ -11,20 +16,21 @@ ;; A QuasiQueue is a list of Xs in *reversed* order. -(struct vm (processes ;; PID -> Process - topics ;; Topic -> Set - flows ;; Flow -> Set +(struct vm (processes ;; Hash + topic-flows ;; Relation + flow-topics ;; Relation + active-handlers ;; Relation next-process-id ;; PID pending-actions ;; QuasiQueue<(cons PID Action)> ) #:transparent) -;; (route PID SID Handlers) -(struct route (process-id sid handlers) #:transparent) +;; (endpoint PID SID Handlers) +(struct endpoint (process-id sid handlers) #:transparent) (struct process (id ;; PID state - interests ;; SID -> List - meta-interests ;; SID -> List + interests ;; Relation + meta-interests ;; Relation ) #:transparent) (struct topic (role pattern virtual?) #:prefab) @@ -35,13 +41,13 @@ ;; PresenceHandler = Topic -> State -> Transition ;; AbsenceHandler = Topic * Reason -> State -> Transition ;; MessageHandler = Topic * Message -> State -> Transition -(struct handlers (topic presence absence message) #:transparent) +(struct handlers (presence absence message) #:transparent) ;; actions is a plain old List, not a QuasiQueue. (struct transition (state actions) #:transparent) ;; Preactions -(struct add-role (sid handlers) #:prefab) +(struct add-role (sid topic handlers) #:prefab) (struct delete-roles (sid) #:prefab) (struct send-message (topic body) #:prefab) (struct spawn (thunk) #:prefab) @@ -68,6 +74,25 @@ (for/list ([role (co-roles (topic-role t))]) (struct-copy topic t [topic-role role]))) +(define (refine-topic remote-topic new-pattern) + (struct-copy topic remote-topic [pattern new-pattern])) + +(define (roles-intersect? l r) + (memq l (co-roles r))) + +;; Both left and right must be canonicalized. +(define (topic-intersection left right) + (and (roles-intersect? (topic-role left) (topic-role right)) + (mgu-canonical (freshen (topic-pattern left)) (freshen (topic-pattern right))))) + +;; True iff the flow between remote-topic and local-topic should be +;; visible to the local peer. This is the case when either local-topic +;; is virtual (in which case everything is seen) or otherwise if +;; remote-topic is also not virtual. +(define (flow-visible? local-topic remote-topic) + (or (topic-virtual? local-topic) + (not (topic-virtual? remote-topic)))) + ;;--------------------------------------------------------------------------- ;; QuasiQueue @@ -93,8 +118,9 @@ (define (make-vm boot) (vm (hash) - (hash) - (hash) + (relation) + (relation) + (relation) 0 (list->quasi-queue (list (spawn boot))))) @@ -118,18 +144,97 @@ (define (perform-action pid action state) (match action - [(add-role sid handlers) ...] - [(delete-roles sid) ...] - [(send-message topic body) ...] - [(spawn thunk) - (match-define (transition initial-state initial-actions) (run-user-code (thunk))) - (define new-pid (vm-next-process-id state)) - (struct-copy vm (enqueue-actions state new-pid initial-actions) - [processes (hash-set (vm-processes state) new-pid (process new-pid - initial-state - (hash) - (hash)))] - [next-process-id (+ new-pid 1)])])) + [(add-role sid topic handlers) (do-subscribe pid sid topic handlers state)] + [(delete-roles sid) (do-unsubscribe pid sid state)] + [(send-message topic body) (route-and-deliver topic body state)] + [(spawn thunk) (do-spawn thunk state)])) + +(define (install-flow state0 source-flow target-topic) + (define state + (struct-copy vm state0 + [topic-flows (relation-add (vm-topic-flows state0) target-topic source-flow)] + [flow-topics (relation-add (vm-flow-topics state0) source-flow target-topic)])) + (if (and (flow-visible? target-topic source-flow) + ;; Only notify if not previously notified, i.e., the routes were + ;; absent in state0. + (not (relation-domain-member? (vm-flow-topics state0) source-flow))) + (for/fold ([state state]) + ([e (in-set (relation-ref (vm-active-handlers state) target-topic))]) + (run-ready state + (endpoint-process-id e) + ((handlers-presence (endpoint-handlers e)) source-flow))) + state)) + +(define ((add-interest sid topic) p) + (struct-copy process p [interests (relation-add (process-interests p) sid topic)])) + +(define (do-subscribe pid sid topic handlers state) + (define e (endpoint pid sid handlers)) + (define topic-previously-known? (relation-domain-member? (vm-active-handlers state))) + ;; Install the handler. + ;; Update the process. + (let ((state + (struct-copy vm state + [active-handlers (relation-add (vm-active-handlers state) topic e)] + [processes (hash-update (vm-processes state) pid (add-interest sid topic))]))) + ;; Add topic <--> flow mappings and fire the appropriate presence handlers. + (if topic-previously-known? + ;; Just tell the local end. The other ends have already heard about this topic. + (for/fold ([state state]) + ([matching-flow (in-set (relation-ref (vm-topic-flows state) topic))]) + (install-flow state matching-flow topic)) + ;; Compute intersections, and tell both ends. + (for/fold ([state state]) + ([matching-topic (in-set (vm-known-topics state))] + [flow-pattern (in-value (topic-intersection topic matching-topic))] + #:when flow-pattern) ;; We know that topic intersects matching-topic. + (let* ((state (install-flow state (refine-topic topic flow-pattern) matching-topic)) + (state (install-flow state (refine-topic matching-topic flow-pattern) topic))) + state))))) + +(define (do-unsubscribe pid sid state) + ;; For each topic in the process's interests, + ;; - for each appropriate endpoint in active-handlers, + ;; - fire the absence handler + ;; - remove the endpoint + ;; - if no handlers remain in active-handlers for that topic, + ;; - for each flow in topic-flows for the topic, + ;; - remove the topic from flow-topics for the flow + ;; - if no topics remain for the flow, + ;; - dualize it using our source topic + ;; - ...?? + +(define (route-and-deliver message-topic body state) + (define endpoints + (for/set ([flow (in-relation-domain (vm-flow-topics state))] + #:when (specialization? message-topic flow) + [matching-flow (co-topics flow)] + [matching-topic (in-set (relation-ref (vm-flow-topics state) matching-flow))] + [matching-endpoint (in-set (relation-ref (vm-active-handlers state) matching-topic))]) + matching-endpoint)) + (for/fold ([state state]) ([e (in-set endpoints)]) + (run-ready state + (endpoint-process-id e) + ((handlers-message (endpoint-handlers e)) message-topic body)))) + +(define (run-ready state pid interrupt-k) + (define old-process (hash-ref (vm-processes state) pid)) + (match-define (transition new-process-state actions) + (interrupt-k (process-state old-process-state))) + (struct-copy vm (enqueue-actions state pid actions) + [processes (hash-set (vm-processes state) pid + (struct-copy process old-process + [state new-process-state]))])) + +(define (do-spawn thunk state) + (match-define (transition initial-state initial-actions) (run-user-code (thunk))) + (define new-pid (vm-next-process-id state)) + (struct-copy vm (enqueue-actions state new-pid initial-actions) + [processes (hash-set (vm-processes state) new-pid (process new-pid + initial-state + (relation) + (relation)))] + [next-process-id (+ new-pid 1)])) (define (enqueue-actions state pid actions) (struct-copy vm state diff --git a/relation.rkt b/relation.rkt index 3300f26..a2417fe 100644 --- a/relation.rkt +++ b/relation.rkt @@ -2,12 +2,16 @@ ;; Relations are equivalent to Hash> and Set>. (require racket/set) +(require racket/match) (provide (rename-out [make-relation relation]) relation? relation->list list->relation + relation->hash + in-relation-domain + relation-empty? relation-count @@ -16,9 +20,13 @@ relation-remove relation-remove-all relation-ref + relation-set + relation-update relation-domain-member? relation-member? + relation-domain + relation-domain-eq? relation-domain-eqv? relation-domain-equal? @@ -62,6 +70,12 @@ [(cons (cons k v) rest) (loop rest (relation-add r k v))] [_ (error 'list->relation "Expected list of key/value pairs")]))) +(define (relation->hash r) + (relation-table r)) + +(define (in-relation-domain r) + (in-hash-keys (relation-table r))) + (define (relation-empty? r) (zero? (hash-count (relation-table r)))) @@ -70,17 +84,17 @@ (define (relation-add r k v) (struct-copy relation r - [relation-table (hash-update (relation-table r) - k - (lambda (old-vs) (set-add old-vs v)) - (relation-set-constructor r))])) + [table (hash-update (relation-table r) + k + (lambda (old-vs) (set-add old-vs v)) + (relation-set-constructor r))])) (define (relation-add-all r k vs) (struct-copy relation r - [relation-table (hash-update (relation-table r) - k - (lambda (old-vs) (set-union old-vs vs)) - (relation-set-constructor r))])) + [table (hash-update (relation-table r) + k + (lambda (old-vs) (set-union old-vs vs)) + (relation-set-constructor r))])) (define (relation-remove r k v) (define old-vs (hash-ref (relation-table r) k (relation-set-constructor r))) @@ -96,10 +110,15 @@ (hash-remove (relation-table r) k) (hash-set (relation-table r) k new-vs))) -(define (relation-ref r k - [failure-result (lambda () (error 'relation-ref "Key not present: ~v" k))]) +(define (relation-ref r k [failure-result (relation-set-constructor r)]) (hash-ref (relation-table r) k failure-result)) +(define (relation-set r k vs) + (hash-set (relation-table r) k vs)) + +(define (relation-update r k updater [failure-result (relation-set-constructor r)]) + (hash-update (relation-table r) k updater failure-result)) + (define (relation-domain-member? r k) (hash-has-key? (relation-table r) k)) @@ -107,6 +126,9 @@ (and (relation-domain-member? r k) (set-member? (hash-ref (relation-table r) k) v))) +(define (relation-domain r) + (hash-keys (relation-table r))) + (define (relation-domain-eq? r) (hash-eq? (relation-table r))) (define (relation-domain-eqv? r) (hash-eqv? (relation-table r))) (define (relation-domain-equal? r) (hash-equal? (relation-table r))) diff --git a/struct-map.rkt b/struct-map.rkt new file mode 100644 index 0000000..6d6f40c --- /dev/null +++ b/struct-map.rkt @@ -0,0 +1,42 @@ +#lang racket/base + +(provide current-struct-mappers + install-struct-mapper! + struct-map + struct-map/accumulator) + +;; Parameter> +(define current-struct-mappers (make-parameter (hash))) + +;; StructType Mapper -> Void +(define (install-struct-mapper! struct-type m) + (current-struct-mappers (hash-set (current-struct-mappers) struct-type m))) + +;; (X -> Y) Struct -> Struct +(define (struct-map f x) + (define-values (result acc) + (struct-map* 'struct-map (lambda (v acc) (values (f v) acc)) (void) x)) + result) + +;; (X Seed -> Y Seed) Seed Struct -> Struct Seed +(define (struct-map/accumulator f seed x) + (struct-map* 'struct-map/accumulator f seed x)) + +(define (struct-map* name f seed x) + (define-values (i skipped) (struct-info x)) + (when (not i) (error name "Cannot retrieve struct-info for ~v" x)) + (define m (hash-ref (current-struct-mappers) + i + (lambda () + (define key (prefab-struct-key x)) + (when (not key) (error name "No mapper for ~v" x)) + (prefab-struct-mapper key)))) + (m f seed x)) + +(define ((prefab-struct-mapper key) f initial-seed x) + (define-values (new-fields final-seed) + (for/fold ([new-fields '()] [old-seed initial-seed]) + ([old-field (cdr (vector->list (struct->vector x)))]) + (define-values (new-field new-seed) (f old-field old-seed)) + (values (cons new-field new-fields) new-seed))) + (values (apply make-prefab-struct key (reverse new-fields)) final-seed)) diff --git a/unify.rkt b/unify.rkt new file mode 100644 index 0000000..fd6124b --- /dev/null +++ b/unify.rkt @@ -0,0 +1,276 @@ +#lang racket/base + +(require racket/set) +(require racket/match) +(require "struct-map.rkt") + +(provide (struct-out variable) + (struct-out canonical-variable) + wild + wild? + non-wild? + variables-in + unify + unify/env + unify/vars + unify-match/vars + freshen + canonicalize + mgu-freshen + mgu-canonical + apply-subst + specialization? + upper-case-symbols->variables + upper-case-symbols->canonical) + +;; A Subst is a Maybe>. +;; TODO: semantics + +;; Compared by eq?, not equal?. In particular, info is not involved in +;; equivalence. +(struct variable (info) + #:property prop:custom-write + (lambda (v port mode) + (display "?" port) + (write (variable-info v) port))) + +;; Compared by equal?, not eq?. The number is a part of the +;; appropriate equivalence relation for canonical-variables. +(struct canonical-variable (index) #:transparent + #:property prop:custom-write + (lambda (v port mode) + (display "?!" port) + (write (canonical-variable-index v) port))) + +;; -> Variable +;; Create a fresh (and hence unconstrained) variable. +(define (wild [base-name '_]) + (variable (gensym base-name))) + +;; Any -> Boolean +;; True iff the argument is a variable or canonical-variable. +(define (wild? x) + (or (variable? x) (canonical-variable? x))) + +;; Any -> Boolean +;; True iff the argument is neither a variable nor a canonical-variable. +(define (non-wild? x) + (not (wild? x))) + +;; Any -> Set +(define (variables-in x) + (let walk ((x x) (acc (set))) + (cond + [(variable? x) (set-add acc x)] + [(pair? x) (walk (car x) (walk (cdr x) acc))] + [(vector? x) (foldl walk acc (vector->list x))] + [(struct? x) (walk (struct->vector x #f) acc)] + [else acc]))) + +;; Variable Any -> Boolean +(define (occurs? var val) + (let walk ((x val)) + (cond + [(eq? var x) #t] + [(pair? x) (or (walk (car x)) (walk (cdr x)))] + [(vector? x) (ormap walk (vector->list x))] + [(struct? x) (walk (struct->vector x #f))] + [else #f]))) + +;; Variable Any Subst -> Subst +(define (extend-subst var val env) + (cond + [(eq? var val) + ;; Avoid trivial tautologies. Less trivial ones are not detected, + ;; but are harmless. + env] + [(occurs? var val) + ;; Occurs check. + #f] + [else + (cons (cons var val) env)])) + +;; Any Subst Set -> Any +(define (chase x env seen) + (if (variable? x) + (cond [(set-member? seen x) x] + [(assq x env) => (lambda (cell) (chase (cdr cell) env (set-add seen x)))] + [else x]) + x)) + +;; Any Any -> Subst +(define (unify a b) + (unify/env a b '())) + +;; Any Any Subst -> Subst +(define (unify/env a0 b0 env) + (let walk ((a0 a0) (b0 b0) (env env)) + (and env + (let ((a (chase a0 env (set))) + (b (chase b0 env (set)))) + (cond + [(variable? a) (extend-subst a b env)] + [(variable? b) (extend-subst b a env)] + [(and (pair? a) (pair? b)) + (walk (car a) (car b) (walk (cdr a) (cdr b) env))] + [(and (vector? a) (vector? b) (= (vector-length a) (vector-length b))) + (for/fold ([env env]) ([ea a] [eb b]) (walk ea eb env))] + [(and (struct? a) (struct? b)) + (walk (struct->vector a #f) (struct->vector b #f) env)] + [else (and (equal? a b) env)]))))) + +;; Any -> (values Any AList) +;; Converts upper-case symbols to variables, making sure that +;; eq? symbols map to eq? variables. +(define (upper-case-symbols->variables x) + (let walk ((x x) (env '())) + (cond + [(upper-case-symbol? x) + (cond [(assq x env) => (lambda (cell) (values (cdr cell) env))] + [else (let ((v (variable x))) (values v (cons (cons x v) env)))])] + [(pair? x) + (define-values (a env1) (walk (car x) env)) + (define-values (d env2) (walk (cdr x) env1)) + (values (cons a d) env2)] + [(vector? x) + (define result (make-vector (vector-length x))) + (values result (for/fold ([env env]) ([i (vector-length x)]) + (define-values (val env1) (walk (vector-ref x i) env)) + (vector-set! result i val) + env1))] + [(struct? x) (struct-map/accumulator walk env x)] + [else (values x env)]))) + +;; Any -> Any +(define (upper-case-symbols->canonical t) + (define env (make-hash)) ;; cheeky use of mutation + (let walk ((t t)) + (cond + [(or (upper-case-symbol? t) (wild? t)) + (cond [(hash-ref env t #f)] + [else (define v (canonical-variable (hash-count env))) (hash-set! env t v) v])] + [(pair? t) (cons (walk (car t)) (walk (cdr t)))] + [(vector? t) (list->vector (map walk (vector->list t)))] + [(struct? t) (struct-map walk t)] + [else t]))) + +;; Any -> Boolean +(define (upper-case-symbol? x) + (and (symbol? x) + (let ((name (symbol->string x))) + (and (positive? (string-length name)) + (char-upper-case? (string-ref name 0)))))) + +;; AList -> AList +(define (flip-env env) + (map (lambda (x) (cons (cdr x) (car x))) env)) + +;; Any Any -> Subst +;; Like unify after upper-case-symbols->variables on both arguments. +(define (unify/vars a b) + (define-values (processed env) (upper-case-symbols->variables (cons a b))) + (define s (unify (car processed) (cdr processed))) + (and s (apply-subst s env))) + +;; Any Any -> Subst +;; Like unify-match after upper-case-symbols->variables on both +;; arguments, extracting bindings only from the first argument. +(define (unify-match/vars a b) + (define-values (pa a-env) (upper-case-symbols->variables a)) + (define-values (pb b-env) (upper-case-symbols->variables b)) + (define s (unify pa pb)) + (and s (apply-subst s a-env))) + +;; Utility used by freshen and canonicalize below. +;; Must visit the term in the order specified by canonicalize +;; below. Here we rely both upon Racket's left-to-right evaluation +;; order and upon defined struct-mappers traversing their arguments in +;; some deterministic order. +(define (freshen* t var-handler canon-handler) + (define env (make-hash)) ;; cheeky use of mutation + (let walk ((t t)) + (cond + [(wild? t) + (cond [(hash-ref env t #f)] + [else (define v ((if (canonical-variable? t) canon-handler var-handler) t env)) + (hash-set! env t v) + v])] + [(pair? t) (cons (walk (car t)) (walk (cdr t)))] + [(vector? t) (list->vector (map walk (vector->list t)))] + [(struct? t) (struct-map walk t)] + [else t]))) + +;; Any -> Any +;; +;; Freshens a term by substituting out variables in the term with +;; fresh variables to produce an arbitrary member of the term's +;; alpha-equivalence-class that shares no variables with the original. +;; +;; Treats canonical-variables just like regular ones, freshening them +;; with new ordinary (non-canonical) variables. +(define (freshen t) + (freshen* t + (lambda (var env) (variable (variable-info var))) + (lambda (var env) (variable (canonical-variable-index var))))) + +;; Any -> Any +;; +;; Canonicalizes a term by substituting out variables in the term with +;; canonical-variables to produce a canonical member of the term's +;; alpha-equivalence-class. +;; +;; Canonical variables are used in a structurally-determined order +;; related to print order: generally, all unseen variables to the left +;; of a term's print representation are given canonical equivalents +;; before those to the right. +;; +;; Canonical-variables may not appear in the input term. +(define (canonicalize t) + (freshen* t + (lambda (var env) (canonical-variable (hash-count env))) + (lambda (var env) (canonical-variable (hash-count env))))) + +;; Any Any -> Any +;; If the arguments unify, applies the substitution to one of them, +;; yielding a most general unifier, and then freshens the result. +(define (mgu-freshen a b) + (define sub (unify a b)) + (and sub (freshen (apply-subst sub a)))) + +;; Any Any -> Any +;; If the arguments unify, applies the substitution to one of them, +;; yielding a most general unifier, and then canonicalizes the result. +(define (mgu-canonical a b) + (define sub (unify a b)) + (and sub (canonicalize (apply-subst sub a)))) + +;; Subst Any -> Any +(define (apply-subst env x) + (let walk ((x0 x)) + (define x (chase x0 env (set))) + (cond + [(pair? x) (cons (walk (car x)) (walk (cdr x)))] + [(vector? x) (list->vector (map walk (vector->list x)))] + [(struct? x) (struct-map walk x)] + [else x]))) + +;; True iff a is a specialization (or instance) of b. +(define (specialization? a b) + (let walk ((a a) (b b)) + (cond + [(wild? b) #t] + [(wild? a) #f] + [(and (pair? a) (pair? b)) + (and (walk (car a) (car b)) (walk (cdr a) (cdr b)))] + [(and (vector? a) (vector? b) (= (vector-length a) (vector-length b))) + (for/and ([aa a] [bb b]) (walk aa bb))] + [(and (struct? a) (struct? b)) + (walk (struct->vector a #f) (struct->vector b #f))] + [else (equal? a b)]))) + +(require racket/trace) +(trace ;;unify/env + ;;upper-case-symbols->variables + ;;apply-subst + ;;specialization? + )