Concurrency - Parallelism Unbound (EECS490Lec23)

Last time, we talked about parallelism. The goal of parallelism is all about using the fact that certain operations are data-independent, allowing us to execute them at the same time without any change in correctness.

We explored this through Fork-Join Parallelism, Vector Parallelism, and Futures, each of which exploited the use of many workers in different ways.

However, while the static and dynamic semantics of parallelism were never at fault, and were almost trivial to design, we realized that they didn’t allow us to reason about how much faster our programs got. After all, our goal was to speed up execution; if we can’t measure that speedup, what choice do we have in getting more out of our computers?

To do this, we defined a cost-semantics, which allowed us to figure out the number of operations an operation had to take. In doing so, we then defined work, the total number of operations needed to complete a task, and depth, the perceived runtime.

If we consider programs as trees, where each connection is a data-dependency, then we realize that the work is the weighted sum of the edges in the graph, while the depth, is the number of steps along the longest path through the graph

Determinism vs. Non-Determinism

All together, we can easily see that parallelism is all about optimizing costs and in getting stuff done. However, due to our rules, we can see that parallelism also has the property of determinism:

$\text{ If } e \Downarrow^{sequential}e' \text{ and } e \Downarrow^{parallel}e'', \text{ then } e'=e''$

In effect, we can say that, through parallelism, we can reason about parallel programs that use these primitives the same we always have, and to great effect.

However, the lower-level primitives you’ll find in 482 and other classes do not behave in this way. This is leads to Concurrency.

Concurrency

• This is all about explicit communication between threads, which share computing resources and allows us to pass messages between each other
• By allowing interaction between two different algorithms running at the same time as each other through messages, which are done through side-effects, we can gain performance but we lose the relative ordering of these messages, as that’s a property of the underlying operating system.

So, once again, imperative programming rears its ugly head. While we’d love to guarantee this lack of data-dependencies, the presence of side-effects leads to problems, which thrusts us into concurrency, as we can’t guarantee the ordering of side-effects

If you haven’t taken 482 yet, it’s good to note here that these primitives are those you’ll see in it. However, in 482, we’ll cover more ways of how people cope with concurrency; for now we’ll simply focus on the primitives and see if we can reason in it.

So, as an example, we can think of the following concurrent program, known as “Milner’s Coffee Machine”.

Milner’s Coffee Machine

The idea of Milner’s Coffee Machine is rather simple. Essentially, let’s pretend we have a coffee machine, which can take either 2 dollars or 4 dollars.

If you’ve taken EECS370 before, you can imagine that we could do this through a finite state automaton. If so, you’d be absolutely correct:

[Initial] --- recieving 2 dollars ---> [state 1] -- recieve $2 -> [state 2]
   ^ ^                                     |                          | 
   | |____________vend tea ________________|                          |
   |__________________________vend coffee_____________________________|

So, if we execute the process normally, we have no problems; if we ask for coffee our vending machine gets 4 dollars, goes from the initial state to state 1, and then to state 2, and then vends the coffee to the user as the user requests coffee.

If we ask for tea, our vending machine gets 2 dollars, turning us from the initial state to state 1, which we then return back to the initial state by vending tea, as the user requests tea

Now, intuitively, it seems like we should be able to have a concurrent vending machine, where we simply allow anyone to send money and get their fix. However, as the sending money and delivering the goods processes share state, we run into problems.

Say we have the following two users:

• User 1, who sends 2 dollars and requests a tea
• User 2, who only sends in 2 dollars and requests coffee

If we simply allow our program to remain as is, we can see that the following could happen:

• The machine receives 2 dollars from User 1
• The machine receives 2 dollars from User 2
• The machine sees the coffee request from User 2, leading to User 1 out of some money and their tea.

This, obviously, sucks. We do not want our consumers to not have their fix, and currently the system has a way for an adversary to get unjust coffee! To correct this machine, we’d need to design new primitives and to, with them, figure out how to create structures that will not accidentally prevent User 1 from getting their fix.

To do so, we’ll need to specify some logic of concurrency, and then use that to reason about processes

Process Calculus

To do so, we’ll define a new syntax, called a process:

Proc p ::= Await(E)            await(e)
        | Stop                 stop
        | Conc(p1,p2)          p1 x p2, or the concurrent execution

These processes refer to the different actors in this event, and how we’d like to run them. Additionally, we’d also like to specify an event syntax, which will refer to the different actions each process can take:

Event E ::= Recv[a](P)                 ?a;P
          | Send[a](P)                 !a;P
          | Choice(E1,E2)              E1 + E2

So we can either wait for a message to send, wait for a message to come to us, or wait for some choice of a set of events.

As these two structures are so connected in so many ways, it benefits us to start and think of these as related. So, for example, we would consider each event as spawning a process, or choosing some process to create, while a process either waits for some event, stops execution, or runs two other processes concurrently.

With all of this notation, we can now turn our abstract vending machine example into the following concrete example:

VendingMachine = await(?2 dollars; await(
                 (?2dollars; await(!coffee; V))
               + (!tea; V)))
TeaUser = await(!2d; await(?tea;stop))
CoffeeUser  = await(!2d; await(!2d; await(?coffee;stop))))
EvilUser = await(!2d; await(?coffee;stop))

So, we notice here that we do not have a channel to send/receive messages. This effectively models protein signaling and/or scheduling processes in a shared memory system.

With our languages created, we need some way to process these languages in some way, through our favorite: judgments!

We do this through a transition judgement, which models the transition from a process P to P’ due to some action, alpha.

$P \rightarrow^{\alpha} P'$

Here, actions have the following syntax:

Action alpha ::= Query[a]  a?
               | Signal[a] a!
               | Empty     epsilon

For some basic rules in this judgement, we could have the following forms:

$\frac{}{\text{await(!a;P)} \rightarrow^{a!}P}$

$\frac{}{\text{await(?a;P)} \rightarrow^{a?}P}$

Here, all we’re saying is that, if we can communicate something, we communicate and transition to the appropriate state. So, if someone asks for a donut, and we have been waiting to send a donut, we can send a donut over and move back to another state, and the requestor can also move back to the initial state.

When we run processes concurrently, then, we’ll need two rules, one for if the first process finishes first, and one for if the second process continues first:

$\frac{P_1 \rightarrow^{\alpha} P_1'}{P_1 \times P_2 \rightarrow^{\alpha} P_1' \times P_2}$

$\frac{P_2 \rightarrow^{\alpha} P_2'}{P_1 \times P_2 \rightarrow^{\alpha} P_1 \times P_2'}$

So, here, we can see that these rules invite non-determinism. As the underlying scheduler is something we’ve abstracted away, we’re unable to determine which process will run if we run both concurrently, so when we’re analyzing program it pays to be careful in doing so. This is because, if there’s a sequence of executions that fails, then the entire program could fail at any moment.

So far, we’ve modelled these executions where the underlying concurrent processes can’t communicate between them. To get at that logic, we need to add two more rules. These will allow us to send and receive signals, if there is no action happening:

$\frac{p_1 \rightarrow^{a!}p_1' \ \ \ \ p_2 \rightarrow^{a?} p_2'}{p_1 \times p_2 \rightarrow^{\epsilon} p_1' \times p_2'}$

$\frac{p_1 \rightarrow^{a?}p_1' \ \ \ \ p_2 \rightarrow^{a!} p_2'}{p_1 \times p_2 \rightarrow^{\epsilon} p_1' \times p_2'}$

We need two forms here to show that either action could send a signal, and either action could receive a signal, so long as the sends and receives match up.

Structural Congruence of Processes

Now, it might seem like a lot of these rules are rather… extraneous. After all, intuitively, we know that p1 x p2 is the same as p2 x p1 , as we wish for the processes to be run at the same time. Thus, if we were able to define some measure of equivalence in processes, it’d make the reasoning harder for a computer, but it would make it easier for us humans, as we can simply exchange one notion for an equivalent notion and proceed, like all of the really cool tricks one can find in mathematics, such as multiplying by 1 and adding 0 “creatively”.

To do so, we’ll define the structural congruence of processes judgement, === , which has the following rules for our sake:

$\frac{}{p_1 \times p_2 \cong p_2 \times p_1}$

$\frac{}{p_1 \times \text{stop} \cong p_1}$

$\frac{}{p_1 \times (p_2 \times p_3) \cong (p_1 \times p_2 ) \times p_3}$

And so on. Again, these will simplify the rules down for us, but might make it harder to construct an algorithm to do the same.

Back to our vending machine!

Now, let’s consider our judgement and proceed, and see what happens.

If we had V x userTea , i.e. someone asks our vending machine for tea, leads to the following sequence of executions:

$V \times U_t = await(?2d;V') \times await(!2d; u_T')$

$\rightarrow await((?2d;V'') + (!tea;V) \times await(?tea; stop))$

$\rightarrow V \times stop$

We could also add more users, but you’d need to create a program and reason about it accordingly, as we know that our current program fails.

Refinements of Process Calculus

As this does not really capture all of the problems inherent to concurrent programming, we’d need to refine these ideas to contain more depth. This could include some of, or all of, the following:

• Sending messages as values instead of some fixed a
• Replication of processes, to allow processes to create themselves to allow for recurrence

• Explicit Communication Channels ( create new channels, sending along a given channel, and receive along a given channel )

  • Like UDP/TCP ports in 485/482/493…
  • Channel references ( channels as values ), which give you private communication between parties

And these ideas, which ensure we’re able to formally reason about concurrency, have slowly made their way into general-purpose languages. For more information, look up “Concurrent ML”.