Lazy Execution: Semantics

Table of Contents

1 Introduction

We study the semantics of lazy execution in Oz, as part of the declarative concurrent model. (Lazy mechanisms exist in sequential languages like Haskell as well.)

The concept we will use to extend the declarative concurrent model is that of a by need trigger. The extended model also remains declaratively concurrent - that is, all interleaved executions of the code lead to logically equivalent stores. Logical equivalence of stores means that all successful executions result in the same state of the store.

2 Demand-driven concurrent model

We add one statement

{ByNeed Proc X}

to the kernel syntax. This is equivalent to

X = {ByNeed Proc}

The effect of executing the code is the same as that of executing

thread {Proc X} end

The scheduling of the execution is what is different. In the case of threading, we know that {Proc X} will be eventually executed by a fair scheduler. In the case of lazy execution, {Proc X} will be evaluated only when Y is needed. Consider the following code:

{ByNeed  proc {$ X} X = 1 end    X}
{Browse X}

In this case, X will be displayed without being evaluated (as _). Suppose now we add a statement which needs the value of X in order to proceed, for example, Y = X+1. Then X will be evaluated by executing the ByNeed procedure.

We now need to explain two aspects:

  1. the semantics of the ByNeed statement, and
  2. the algorithm to determine whether a variable is needed.

3 Semantics of ByNeed

We add one concept, that of the by-need trigger. A trigger is a pair \((C,A)\), where

  1. \(C\) is an activation condition which is a Boolean expression, and
  2. \(A\) is an action, which is a procedure to be evaluated when the condition is true. This procedure is evaluated at most once, that is, when the activation condition is first true. When the procedure has thus been evaluated, we say the trigger has been activated.

To explain the semantics of the ByNeed statement, we thus need the following

  1. The concept of a trigger store, which is a collection of triggers.
  2. Trigger creation
  3. Trigger activation
  4. The algorithm for needing a variable.

3.1 Extension of execution state

A trigger is a pair trig(p,x) of a procedure x and a variable y. In addition to the SAS, we add a trigger store to the execution state. So the execution state now becomes a triple $$(MST, \sigma, \tau)$$ where \(\sigma\) is the single assignment store, and \(\tau\) is the trigger store.

3.2 Trigger creation

The semantic statement is

{ (ByNeed <p> <x>), E } % <p> is a procedure value, <x> is a variable

where E is the current environment.

The semantic actions taken when the above statement is at the top of the currently active semantic stack (recall that in the declarative concurrent model, we have a multistack), is

  1. If E(<x>) is not determined, then add trig(E(<p>), E(<x>)) to the trigger store.
  2. If E(<x>) is determined, then create a new thread with the single statement
( {<p> <x>},  E )

Question: Why do we create a new thread? Why don't we execute it in the same thread where <x> is needed? Will such an execution be consistent with causal ordering?

Note: A situation in which condition 2 can arise: a thread first binds <x>, and another thread creates the trigger for <x>. When the second thread executes, E(<x>) is possibly determined.

3.3 Trigger activation

If the trigger store contains trig(<p>, <x>) and the execution needs <x>, then

  1. Remove trig(<p>, <x>) from the trigger store.
  2. Create a new thread with the single statement
( {<a> <b>}, {<a> -> p, <b> -> x } )

where <a> and <b> are distinct variables.

T1:  | x is needed                   <....... Trigger condition
     | remove trig(p,x)
     | create T2
     |
     |------+
     |  T2: | Evaluate {p x}         <....... Triggered action
     |      |
     |      |
     V      V

3.4 Needing a variable

We now define what is means for a variable to be needed. The definition must ensure that declarative concurrency is valid - that is, all interleaved executions must lead to logically equivalent stores.

A variable X is needed if some statement is suspended, waiting for X to be determined, or when X is already determined.

We will consider some cases, and examine in each, whether the variables are needed.

3.4.1 Example 1

thread {ByNeed proc {$ A} 3 end X} end
thread {ByNeed proc {$ B} 4 end Y} end
thread Z = X+Y end

(Assume that + is a suspendable operation, which suspends when one of its operands is unbound.)

In this case, X and Y are needed.

3.4.2 Example 2

A variable is needed, when it is determined. This definition is needed to make the model declaratively concurrent - in particular, to ensure that if some interleaved execution fails, then all interleaved executions fail.

thread {ByNeed proc {$ A} A=3 end X} end
thread X = 2 end
thread Z = X+4 end

Suppose the first thread executes. This creates a trigger for X. Now, if the third thread executes, then X is needed, the trigger will be activated, and X will be bound to 3, and Z to 6. Assuming a fair thread scheduler, the second thread will be executed eventually, leading to a unification error.

Suppose X is bound to 2 by the second thread. If now the third thread executes, Z is bound to 6. Suppose we do not consider X needed, the trigger will not be activated, there will be no unification error, and this interleaved execution will succeed.

The way to prevent this is to say that X is needed when it is already determined. In this way, the second execution also results in unification failure.

3.4.3 Example 3

thread {ByNeed proc {$ A} A = 3 end X} end
thread X = Y end
thread if X==Y then true end end

Is X needed here?

X is bound to Y, but it is not determined since Y is not bound to a value.

So the comparison X==Y will not trigger X.

Another way to think about it: is it necessary to determine X? Can the execution succeed if X is considered not needed in the above code?

(To see this:

local X Y in
   {Browse X}
   thread {ByNeed proc {$ A} A = 3 end X} end
   thread {Delay 10} X = Y end
   thread {Delay 10000} if X == Y then {Browse true} end end
end

Observe that there is no failure exception thrown in the emulator window, and X remains undetermined in the Browser.)


Date: 2014-09-25T08:21+0530

Author: Satyadev Nandakumar

Org version 7.9.3f with Emacs version 24

Validate XHTML 1.0