Mutable State and Transactions: Bank Account Example

In Vodka, there are no mutable variables. By making use of the state-fullness of function symbols, however, we can easily implement them in the language itself, combining a never-returning function state with a getter and a setter function. 

# define a primitive mutable meory cell

new initVar;

def initVar(x):
{
    new cell.get;
    new cell.set;

    new state;
    
    def state(x) & cell.set(y): state y & return ();
    def state(x) & cell.get():  state x & return x;
    
    return(cell) & state(x);
}


# example

a = initVar(7);

a.set(9);

print a.get();

# output: 9;

Introducing Software Transactions

The memory cell presented above is of course a very simple model that suffers from all problems commonly associated with mutable state. As one of the classical examples, we consider two processes that concurrently access a shared bank account, simultaneously trying to withdraw and deposit $100: 

accountBalance = initVar(1000);

print("Initial balance:");

print(accountBalance.get());


new blockA;
new blockB;

def blockA(t):
{
    print "    A begin";
    
    accountBalance.set(accountBalance.get() - 100);

    print "    A end";
    
    return();
}

def blockB(t):
{
    print "    B begin";

    accountBalance.set(accountBalance.get() + 100);
    
    print "    B end";
    
    return();
}


blockA() & blockB();

print("The new balance is:");

print(accountBalance.get());

# output: most likely 900 or 1100

By extending the interface a little bit, however, we can build more advanced models. As one example, we can design a software-transaction model, where mutable cells keep a version number that is incremented on every change. Variables must then be entered into a transaction, saving their current version number and yielding a copy that is only valid within the transaction. Upon committing a transaction, an attempt is made to lock all entered variables, succeeding only if each variable's original has not been altered concurrently (the version number is used to check that). If all variables can be locked successfully, they are unlocked, each one taking the new value from the temporary copy and updating the version tag if the new value differs from the old. If any variable has been modified in the meantime, the locking fails, all other variables are unlocked without modification and the commit operation signals a failure.

The regular way to handle such a failure is to retry the operation in a new transaction. In fact, we can define a higher-order function atomic that does just that, repeatedly executing another function with a fresh transaction until the commit succeedes. 

# Wrap up functions as atomic blocks

new atomic;

def atomic(f):
{
    t = initTransaction();

    r = f(t);
    
    if t.commit():
        returnto.atomic r;
    else:
        returnto.atomic atomic(f);
}

The bank account example can thus be re-implemented in a safe way: 

persistantAccountBalance = initTransactionVar(1000);

print("Initial balance:");

print(persistantAccountBalance.get());


new blockA;
new blockB;

def blockA(t):
{
    print "    A begin";
    
    accountBalance = t.enter(persistantAccountBalance);
    
    accountBalance.set(accountBalance.get() - 100);
    
    print "    A trycommit";
    
    return();
}

def blockB(t):
{
    print "    B begin";

    accountBalance = t.enter(persistantAccountBalance);
    
    accountBalance.set(accountBalance.get() + 100);
    
    print "    B trycommit";
    
    return();
}


atomic(blockA) & atomic(blockB);

print("The new balance is:");

print(persistantAccountBalance.get());


# output: exactly 1000