eighty-twenty

This is the second part of a series of three articles on modelling actor-like systems^1 2 using PLT Redex.

• Part I: The Functional Fragment: ISWIM in Redex
• Part II: The Communicating Fragment: Actors in Redex
• Part III: Efficiency vs. Nondeterminism

Like the previous post, this post is written as a literate Racket source file, and is licensed CC-BY 4.0. You can download it and run it yourself.

The Communicating Fragment: Actors in Redex

Here, we build on the functional fragment language that we developed in Part I, adding communication primitives to it.

Here’s a little program in the extended language. It creates an initial configuration holding a “boot” actor, which spawns two more actors, which each send themselves a message:

(boot-actor (spawn (send (self) 0))
            (spawn (send (self) 0)))

Nondeterminism enters the mix in a big way at this point, even for such a small, simple program as this. The traces for this example show a lot of branching, and the more complex a program is, the more possible interleavings it will have:

Preliminaries

As before, we need the Racket #lang header, and we need to load Redex itself. Since we’re also making use of the model we developed last time, we load that too. It is contained in a file called redex-iswim.rkt in the same directory as this file.

#lang racket
(require redex)
(require "redex-iswim.rkt")

Syntax

We define our Actor language by extending the syntax of the plain ISWIM-like language we developed last time.

We add four new kinds of primitive expressions, one new primitive type, and a bunch of structure related to representing entire groups of actors syntactically.

A syntax extension is declared by invoking define-extended-language with the name of the extended language, ISWIM+Actors, and the name of the language to be extended, ISWIM, which was imported from redex-iswim.rkt above.

(define-extended-language ISWIM+Actors ISWIM

Expressions, Values, Process IDs and Contexts

Starting with the new expressions, we let actors send messages to peers with (send ...), receive messages sent to them by their peers with (receive), discover their own identities with (self), and spawn new actors with (spawn ...).

  (expr ....
        (send expr expr)   ;; sends the second arg to the first arg, a PID
        (receive)          ;; blocks, waiting for the next message
        (self)             ;; evaluates to the PID of the calling actor
        (spawn expr ...))  ;; spawns a new actor which performs the exprs.

Values in our extended language include all the values from before, namely numbers, strings, booleans and so on, plus the addition of Process IDs, PIDs.

  (value ....
         pid)

We choose to represent PIDs using symbols—variable names—since that way, we can use Redex’s built-in name-freshening machinery to guarantee that a newly-spawned actor receives a genuinely fresh PID that is shared by no other actor in the group.

  (pid variable-not-otherwise-mentioned)

Our evaluation contexts also need to be updated for the new syntax. Here, only send expressions involve evaluating subterms before being processed, so we have only a small change to make to the context nonterminal from ISWIM.

  (context ....
           (send context expr)
           (send pid context))

Writing it this way forces evaluation order in a send to be left-to-right, consistent with all the other syntactic forms in the language.

Configurations

The main difference between the reduction relation we’ll build and the one we built last time is that this one will operate on whole configurations of actors rather than on individual ISWIM expressions.

We introduce a new syntactic category, configuration, which represents a pair of a queue of messages yet to be delivered, and a process table.

  (configuration ((queued-message ...) (actor ...)))

A queued message is a pair of an ISWIM value and the PID that it is addressed to. (The => is punctuation which makes reading terms in interactive use easier.) I’ve chosen the convention of adding new entries at the right-hand end of the queue, and removing entries from the left-hand end.

  (queued-message (value => pid))

An entry in the process table, an actor, is a triple of the actor’s PID, its mailbox, and its current program state in the form of an expression in the extended ISWIM+Actors syntax. The mailbox is a queue of messages, keeping the same convention described above.

  (actor (pid : mailbox expr))
  (mailbox (value ...)))

We didn’t introduce any new binding constructs, so we don’t have to mention #:binding-forms like we did for ISWIM.

Operational Semantics

Reduction Rules

While Redex does offer extend-reduction-relation, it doesn’t work well for us here because we are going to be interpreting ISWIM’s notions of reduction with a new kind of context: with configurations carrying contexts instead of plain contexts alone.

Instead, we define a new reduction relation.

(define ISWIM+Actors-red
 (reduction-relation ISWIM+Actors

Our first rule, send, queues the message to be sent and the pid naming its target in the configuration’s buffer, and replaces the (send ...) expression with #t.

  (--> ((queued-message ...)
        (actor_0 ... (pid_1 : mailbox (in-hole context (send pid value_0)))
         actor_1 ...))

       ((queued-message ... (value_0 => pid))
        (actor_0 ... (pid_1 : mailbox (in-hole context #t))
         actor_1 ...))

       send)

Notice the “actor_0 ...” and “actor_1 ...” subpatterns. These allow Redex to pick any actor that matches the rest of the pattern, nondeterministically. As we will see, such subpatterns also occur in each of the remaining rules.

After a send rule has placed a message addressed to some pid in the configuration’s buffer, the deliver rule then takes it, finds the actor named pid in the process table, and places the message in its mailbox. Everything else is left unchanged.

  (--> (((value_0 => pid) queued-message ...)
        (actor_0 ... (pid : (value_1 ...        ) expr) actor_1 ...))

       ((queued-message ...)
        (actor_0 ... (pid : (value_1 ... value_0) expr) actor_1 ...))

       deliver)

But what if the addressee no longer exists? This can’t happen with this version of the language (see exercises), but could happen if we were to alter the language in one of any number of simple, harmless ways. The failed-delivery rule simply drops buffered messages in the case that the addressee is not in the process table.

  (--> (((value_0 => pid) queued-message ...) ((pid_0 : mailbox expr) ...))
       ((                 queued-message ...) ((pid_0 : mailbox expr) ...))
       (side-condition (not (memq (term pid) (term (pid_0 ...)))))
       failed-delivery)

The receive rule selects the next ready message from an actor’s mailbox. The way the rule is written, it is only applicable if the mailbox is nonempty. This automatically makes actors block if they invoke (receive) when they have empty mailboxes: their term is simply stuck until some matching message comes along.

  (--> ((queued-message ...)
        (actor_0 ... (pid :
                          (value_0 value_1 ...)
                          (in-hole context (receive)))
         actor_1 ...))

       ((queued-message ...)
        (actor_0 ... (pid :
                          (        value_1 ...)
                          (in-hole context value_0  ))
         actor_1 ...))

       receive)

The self rule replaces occurrences of (self) that are (a) in some evaluation context that is in turn (b) in some actor that is in turn (c) in our global configuration. We know syntactically which actor it is that’s invoking (self) so it’s easy to choose which pid to replace (self) with.

  (--> ((queued-message ...)
        (actor_0 ... (pid : mailbox (in-hole context (self))) actor_1 ...))

       ((queued-message ...)
        (actor_0 ... (pid : mailbox (in-hole context pid   )) actor_1 ...))

       self)

Finally, spawn is handled by allocating a fresh PID using Redex’s fresh side-condition and turning the exprs into a new actor alongside its parent.

Here I’ve chosen to replace the (spawn ...) expression with the new actor’s PID, but this isn’t absolutely necessary; something like #t would do.

  (--> ((queued-message ...)
        (actor_0 ... (pid_1 : mailbox (in-hole context (spawn expr ...)))
         actor_1 ...))

       ((queued-message ...)
        (actor_0 ... (pid_1 : mailbox (in-hole context pid_new))
         actor_1 ... (pid_new : () (begin expr ...))))

       (fresh pid_new)
       spawn)

Finally, we copy the beta, delta, begin-one, begin-many, if-true, if-false and unfold rules from ISWIM verbatim.³ Because they’re exactly the same as before, I’ve omitted them from the write-up; they are, however, still in the program source code.

;; (ISWIM notions of reduction omitted from presentation)

Following these ISWIM notions of reduction, we define what the ==> shortcut arrow means. Here it’s expressed in terms of our configurations, not just in terms of context the way that plain ISWIM assigned meaning to it. This lets the plain ISWIM notions of reduction function in any reducible actor in the process table.

  with
  [(--> ((queued-message ...)
         (actor_0 ... (pid : mailbox (in-hole context A)) actor_1 ...))

        ((queued-message ...)
         (actor_0 ... (pid : mailbox (in-hole context B)) actor_1 ...)))

   (==> A B)]))

Metafunctions

The delta, subst-all and let metafunctions are identical to those presented last time, so I’ll omit them in this write-up. (They are in the source code, however.)

;; (Metafunctions `delta`, `subst-all` and `let` omitted)

However, for our new system we do need one new metafunction, boot-actor, which takes a sequence of exprs and places it in a starting configuration for the reduction relation to operate on.

(define-metafunction ISWIM+Actors
  boot-actor : expr ... -> configuration
  [(boot-actor expr ...) (() ((boot : () (begin expr ...))))])

Examples and Tests

As before, we put a few simple tests in a test submodule.

(module+ test

This checks that ISWIM reductions can happen in a running actor. The expected result (() ((boot : () 124))) is a configuration with an empty buffer and with one actor, whose PID is boot, with an empty mailbox and an expression that is a value 124.

  (test-->> ISWIM+Actors-red
            (term (boot-actor ((lambda (x) (+ x 1)) 123)))
            (term (() ((boot : () 124)))))

Here we test learning our own PID and sending a message to ourselves: the boot actor sends itself 123, receives it, and adds one to it.

  (test-->> ISWIM+Actors-red
            (term (boot-actor (send (self) 123) (+ (receive) 1)))
            (term (() ((boot : () 124)))))

Here we check that let works as we expect.

  (test-->> ISWIM+Actors-red
            (term (boot-actor (let ((w (self))) w)))
            (term (() ((boot : () boot)))))

Here we check spawning of multiple actors.

  (test-->> ISWIM+Actors-red
            (term (boot-actor (spawn 1) (spawn 2)))
            (term (() ((boot : () pid_new1) (pid_new : () 1) (pid_new1 : () 2)))))

Here we check cross-actor message sending.

  (test-->> ISWIM+Actors-red
            (term (boot-actor (let ((w (self))) (spawn (send w 123)) (receive))))
            (term (() ((boot : () 123) (pid_new : () #t)))))

Here we check communication of PIDs, not just regular ISWIM values.

  (test-->> ISWIM+Actors-red
            (term (boot-actor (let ((w (self))) (spawn (send w (self))) (receive))))
            (term (() ((boot : () pid_new) (pid_new : () #t)))))

Here we check recursion combined with message sending.

  (test-->> ISWIM+Actors-red
            (term (boot-actor
                   ((rec loop (lambda (count) (if (= count 0)
                                                  0
                                                  (begin (send (self) count)
                                                         (loop (- count 1)))))) 3)))
            (term (() ((boot : (3 2 1) 0)))))

Nondeterminism is very slow

Try the following command with this file loaded in DrRacket:

(traces ISWIM+Actors-red
        (term (boot-actor
               (spawn (send (self) 0))
               (spawn (send (self) 0)))))

Notice the large number of intermediate terms before the final answer is computed! There are many possible interleavings of execution of this little program, leading to a lot of nondeterminism.

The corresponding test takes a correspondingly long time to execute.

  (test-->> ISWIM+Actors-red

            (term (boot-actor
                   (spawn (send (self) 0))
                   (spawn (send (self) 0))))

            (term (() ((boot : () pid_new1)
                       (pid_new : (0) #t)
                       (pid_new1 : (0) #t))))))

Examples that are even slightly larger take a very, very long time to run. Here is an example I’ve commented out because of its prohibitive slowness.

  ;; (test-->> ISWIM+Actors-red
  ;;           (term (boot-actor
  ;;                  (let ((counter (self)))
  ;;                    (spawn (send counter 1)
  ;;                           (send counter 1)
  ;;                           (send counter 1)))
  ;;                  ((rec loop (lambda (count)
  ;;                               (loop (+ count (receive))))) 0)))
  ;;           (term ???))

What can we do about this slowness? Part III will look into some possibilities.

Conclusion

We have extended our model of an ISWIM-like language with Actor-style facilities including spawn, process IDs, and message sending and receiving. We kept the ISWIM notions of reduction, but placed them into a new kind of context: configurations. We also added new rules that act on configurations directly to perform the Actor-related effects that programs written in our language can now request. In Part III, we will explore ways of reducing inessential nondeterminism in order to gain efficiency.

Exercises

1. (Easy.) Alter the receive rule to nondeterministically choose any of the queued messages in the mailbox. This removes the axiom of ordered delivery from the model.

2. (Easy.) Add a rule called message-loss that nondeterministically leads to the loss of a sent message. From which queue did you choose to remove the message? What other possibilities exist? Can you make an analogy between the different queues in a configuration and the buffers and queues in your operating system kernel and in your Ethernet cards, your LAN switches, and your routers?

   Hint: Because making this change introduces nondeterminism, you will want to add additional possible outcomes to the test-->> forms in the test submodule.

3. (Easy.) Develop an argument for why programs written in our Actor language will never invoke the failed-delivery delivery rule. What assumptions do you need to make for your argument to hold?

4. (Medium.) Add support for a new (quit) expression that terminates the invoking actor and removes it from the process table.

5. (Hard.) Add a garbage-collection rule which removes “finished” actors from the configuration’s process table. When is an actor “finished”? Is there an appropriate syntactic criterion you can use to decide? Is your approach sound? Is it complete?

6. (Medium.) Add support for Erlang-style monitors (see also here) and exit-notification-messages.

References and Footnotes