explicit-state

We will deal with explicit state, in a sequential setting.

Principle of abstraction: Programs can be separated into specification and implementation. Specification: A contract defining how the system should behave Implementation: How the specification is realized.

Declarative and imperative programming both support this. However, when a system "grows", declarative programs have to be changed. The only way for a declarative program to know more about the external world, is by having extra arguments (for example, more accumulators). This means that not only the implementation, but the specification also changes.

Having internal state within the program helps us to model internal state as extra information within the program while keeping the specification the same as before. So imperative program supports this kind of abstraction better.

A system that supports the principle of abstraction has

Characterized by encapsulation, compositionality and instantiation.

Each component is a part of the system.

Specifies an interface: how the component is seen from the "outside".

In component-based programming, we can compose components: build a new component that contains the original one.

We can model state, even in the declarative style.

fun {SumList Xs S}
    case Xs
    of nil then S
    [] X|Xr then {SumList Xr X+S}
end

The code above is a declarative code which sums up the elements in a list. Consider the call {SumList [1 2 3] 0}. The last argument to the recursive calls takes the sequence of values 0, 1, 3, 6. This sequence can be seen as a state as per the definition.

Definition An explicit state in a procedure is a state whose lifetime extends over more than one procedure call, without being one of its argumnents.

Explicit state cannot be expressed in the declarative model. For that, we need a new concept called a cell.

local
   C = {NewCell 0}
   SumList
in
    proc {SumList Xs}
        case Xs
        of nil then skip
        [] X|Xr then
           C:=@C+X
           {SumList Xr}
        end
    end
    {SumList [1 2 3 4]}
    {Browse @C}
end

There are two operations allowed on cells

• := sets the content of the cell
• @ accesses the content of the cell

Definition A cell is a pair of a name, and a reference into the SAS.

Names are unforgeable, hence a cell is a secure ADT.

We introduce a new store called the mutable store. The cells are part of the mutable store.

There are now two stores: the SAS, which is immutable, and the mutable store of the cells.

.....................     .......................
.                   .     .                     .
.                   .     .                     .
.    w:10           .     .    cell1: w         .
.    x:2            .     .    cell2: x         .
.                   .     .                     .
.                   .     .                     .
.                   .     .                     .
.                   .     .                     .
.....................     .......................
   IMMUTABLE STORE        MUTABLE STORE consisting of cells

We add two new statements to the declarative sequential model of Chapter 2, to handle cells.

The statement that creates a cell is

{NewCell Cell InitialValue}

Semantics

In addition to the single assignment store (and the trigger store if we consider lazy evaluation), we create a mutable store. This store is initially empty. The mutable store contains cells which are pairs of the form x:y where x and y are variables of the SAS. x is always a name. y can be any partial value.

The execution state is now a tripe (Stack, SAS, Mutable).

The semantics for the ({NewCell Cell InitialValue}, Env) statement is:

• Create a new name n in SAS
• Bind E(Cell) and n in SAS
• If binding succeeds, add the pair E(Cell):E(InitialValue) in the Mutable store
• Otherwise, raise an error.

The statement that modifies the value of a cell is:

{Exchange Cell OldValue NewValue}

(OR)

OldValue=(Cell:=NewValue)

This statement atomically binds OldValue to the old content of Cell, and sets the new content of Cell to be NewValue. Another syntax for the exchange statement is using the := operator. Usually we do not care about the old value of the cell, so the syntax simply reads

Cell:=NewValue

Semantics

The semantics of ({Exchange Cell OldValue NewValue},E) is

+If the activation condition, E(Cell) being determined, is false, suspend execution. Otherwise, we do the following.

1. If E(Cell) is not bound to the name of a cell, then raise an error
2. If the mutable store contains E(Cell):w, then do the following
   • Update the mutable store to E(Cell):E(NewValue)
   • Bind E(OldValue) and w in the store.

We just have to modify the definition of reachability to deal with the new operations. In addition to the previous cases, a variable y is reachable if the mutable store contains x:y and x is reachable.

If a variable x becomes unreachable, and the mutable store contains x:y, we remove this pair from the MS. (Note that y is not necessarily reclaimed in SAS.)

Reversing a list with cells:

fun {Reverse Xs}
   R = {NewCell nil}
in
   for X in Xs do Rs := X|@Rs end
   @Rs
end

A cell is semantically, a pair of the form x:y. Hence we now have to distinguish the equality of cells from the equality of their contents.

The concept of sharing or aliasing is when two identifiers refer to the same cell.

X = {NewCell 0}
Y = X            % Y is an alias of X
Y := 10
{Browse @X}      % displays 10

When any alias changes the content of the cell, all the aliases see the changed content. This makes reasoning about the program difficult (In the previous example, if you just consider the statements in which X appears, you cannot compute the current value of X.)

X = rec(f:1)
Y = rec(f:2)
{Browse X==Y}    % displays true

X = {NewCell 0}
Y = {NewCell 0}
{Browse X==Y}    % displays false
{Browse @X==@Y}  % displays true. However, this may change subsequently
Y:=1
{Browse @X==@Y}  % displays false now

Z = X
{Browse X==Z}    % displays true

Suppose we implement a stack as a list, which supports operations for pushing, popping, and to check emptiness. We might implement it in the following manner.

local
  fun {NewStack} nil end
  fun {Push E S} E|S end
  fun {Pop S} if {isEmpty S}==false then S.1 end
  fun {IsEmpty S} S==nil end
in
  local X Y in
    X = {NewStack}
    {Browse {Pop {Push 2 {Push 1 X}}}} % displays 2
end

This implementation, where there is no encapsulation of the data and the procedures acting on it, is called an unbundled implementation or an Abstract Data Type (ADT).

The disadvantage is that if a programmer guesses that the stack is implemented as a list, (s)he can call {Length S}, which is not an operation that is meant to be performed on a stack.

How can we ensure that a user goes only through the procedures that are provided in the ADT? We can use names for this purpose.

We will first introduce the notion of a wrapper/unwrapper pair of functions. To secure some value X, what we will do is to "lock" X inside a function, with a name - we call this they "Key". This function expects a key as input. If the given key is correct, we get the value of X.

Unwrap is a function which can unlock the wrapped version of X by giving the correct key.

Two things together ensure security: NewName returns a unique name, and the Key thus obtained is hidden from the outside by lexical scoping.

declare

proc {NewWrapper ?Wrap ?Unwrap}
    Key={NewName} % Unique key.
in
    % returns a function, which serves as
    % the "wrapped version" of X
    fun {Wrap X}
       fun {$ K} 
         if K==Key then X end 
       end
    end

    % function which takes a wrapped input and
    % returns the unwrapped value
    fun {Unwrap W}
       {W Key} % Calls wrapped version with the correct key
    end 
end

% Usage
S = [1 2 3]             
SecureS = {Wrap S}    % Note: SecureS is a function!
T = {Unwrap SecureS}  % T = [1 2 3]
                      % {Unwrap {Wrap S}}==S
% {Length SecureS} will fail

Using the wrap/unwrap pair, we can now implement a secure unbundled stack.

local Wrap Unwrap in
    {NewWrapper Wrap Unwrap}

    % Note that the wrapped stack is a function, not a list.

    fun {NewStack} {Wrap nil} end 
    
    fun {Push E S} {Wrap E|{Unwrap S}} end

    % Pop binds the top of the stack in E and returns the smaller
    % stack. 
    fun {Pop S ?E}
        case {Unwrap S}
        of H|T then 
            E=H
            {Wrap S1}
        end
    end

    fun {IsEmpty S} {Unwrap S}==nil end
end

Now, the only way a user can mainpulate the stack is through the set of four functions above. A call of the form {Length {NewStack}} will fail.

The above two implementations were "unbundled" implementations. We can implement declarative bundled implementations as well. We will change two design choices at the same time and consider a secure, bundled, stateful stack. We will see that we do not need names here: security is ensured just by lexical scoping.

fun {NewStack}
    C={NewCell nil}
    proc {Push E} C:=E|@C end
    fun {Pop} case @C of X|S1 then C:=X1 S end end
    fun {IsEmpty} @C==nil end
in
    stack(push:Push pop:Pop isEmpty:IsEmpty}
end