Written Assignment 6

In this homework, you will be working with a core, concurrent language, also known as a process calculus.

Our version is loosely modeled after Robin Milner’s CCS. We    rst set up the language grammar.

Num n ::= 0 j 1 j 2 j

Var v ::= x j y j z j

Exp e ::= v j n j e1 + e2 j e1    e2 j
BExp b ::= true j false j e1 < e2 j
Chn C ::= A j B j C j

Prc P; Q ::= done j v ( C; P j e ) C; P j mk CfP g j [b] P j P + Q j P jQ

In words, we have the following components:

Numbers (0, 1, . . . ) Variables (x, y, . . . )

Expressions possibly involving variables (x + 0, 3 5) Boolean expressions (x < 0)

Channel names (A, B, . . . )

Processes are built out of several components. Following the order in the grammar:

The done process, which doesn’t do anything.

Receiving a message from a channel, and using it in another process. Sending a message to a channel, then continuing as another process. Declaring a new channel for use in a process.

Running a process if some boolean condition is true. Running one process or another process.

Running two processes in parallel.

We will work with an operational semantics for processes, except steps may have labels:P ! Q means that P steps to Q without sending or receiving anything externally. (Components within P may exchange messages before stepping to Q.)


1

We write L for any label: send, receive, or none.  We assume that we have a standard step relation for

expressions and boolean expressions: e ! e0 .
    • Stepping processes (15)

Step the following processes.  Note that there are many possible traces for each process.  Just show one

trace where (i) the rst step has a label of the form I; m, and (ii) the last step has a label of the form O; n. (Perhaps I and O are special input/output channels, like the input and output of the main thread.)

We’ve done the    rst one for you.

    0. x ( I; x ) A; donejy ( A; y + 1 ) O; done


I;42
! 42 ) A; donejy ( A; y + 1 ) O; done

! donej42 + 1 ) O; done

! donej43 ) O; done

O;43
! donejdone

    1. x ( I; x + 1 ) O; done

    2. x ( I; ([x > 12] 100 ) O; done) + ([x   12] 5 ) O; done)

    3. x ( I; x  1 ) O; donejx ( I; x + 1 ) O; done

    4. x ( I; x ) A; donejy ( A; y + y ) O; done

    5. mk Afx ( I; x ) A; donejy ( A; y + y ) O; doneg

    • Writing processes (10)

Write down a process that models the following scenarios. Demonstrate how the rst process works by giving one trace. For the second process, explain why it cannot make any progress.

    1. Two communicating threads. The rst adds one to the input and passes to the second, the second adds two and passes it back to the rst, and the rst adds three and sends to output.

    2. Two deadlocked threads. Both threads should be trying to receive on a channel, but the combined process should not be able to reduce. Note: your process should not be able to reduce, even if there are some external inputs or outputs on channels besides I and O.


2
    • Recursive processes (5)

To handle recursive processes, we extend the grammar with process variables and de nitions, and allow process variables to show up in processes:

PVar ::= X j Y j Z j

PDef ::= X , P

Prc P; Q ::= X j

Note that process de nitions can be recursive|the process P on the right-hand side of X , P can mention

X (or other process variables). We also introduce a step rule to unfold a de nition:

        ◦ , P X !  P
    1. A doubling server. Write a process that continually listens to a channel A, receives a value, doubles the value and outputs it on a channel B. Your process should loop: it should be able to handle an arbitrary number of inputs to A, not just one input.

    2. A stateful server. So far, all our processes have been state-less: they do not remember previous messages that have been sent or received. While we could augment processes with a notion of local state by adding a store, it turns out hat we can borrow an idea from the calculus and use the process itself to represent the state.

To see how this works, write a process that continually listens to a channel A. For every odd ( rst, third, fth, . . . ) incoming request, your process should output zero on channel B. For every even (second, fourth, sixth, . . . ) incoming request, your process should double the input and output on channel B. (Hint: you should probably write two de nitions, representing the behavior in odd counts, and the behavior in even counts.)


For each part, your solution should consist of (i) one or more de nitions, and (ii) a main process (which might be just a process variable). Demonstrate how your processes work by composing in parallel with a client process and showing a trace. Your client processes do not need to be very complicated, perhaps they just issue 1-2 requests. You can skip over uninteresting steps in the reduction.
























3