Function Symbols and Function Bodies

new philosopher: Unit --> Void;

def philosopher():
{
    takeForks();
    eat();
    releaseForks();
    think();
    philosopher();
}

Function Bodies may Link Multiple Function Symbols

In the code above, subroutines are used to take and release two forks simultaneously. This is one of the nontrivial parts of traditional solutions where each fork is modeled by one synchronization primitive that allows only individual access control, but not in coaction with others. A naive implementation can lead to deadlock, e.g. when all philosophers hold only their respective left fork and wait for the other to be released.

Here, the language allows to circumvent this issue by declaring a function body that is only executed after multiple function symbols have been invoked:

new leftFork: Unit --> Void;
new rightFork: Unit --> Void;

new takeForks: Unit --> Unit;
new releaseForks: Unit --> Unit;

def leftFork() & rightFork() & takeForks(): return();
def releaseForks(): leftFork() & rightFork() & return();

As opposed to the function symbols labeled leftFork and rightFork, which are of type Unit --> Void, the functions takeForks and releaseForks are of type Unit --> Unit. The type Void literally describes the empty type that does not contain any values. A call to a function declared to return a Void result will never terminate. The type Unit, however, contains the single value () and functions declared to return Unit (or any other type) may return control to their caller.

In this example, we have written down type annotations explicitly. The type system of the current Vodka implementation, however, is a dynamic one, so we could have chosen to omit them. But in those cases where explicit types are given, the compiler will inject runtime checks into the code that will produce error messages when the type assertions are violated.

The meaning of the function body definitions in the above source block is as follows:

If there are calls to takeForks, leftFork and rightFork present at the same time, control will be returned to the caller of takeForks, while the pending calls are consumed. Since this is the only function body attached to the function takeForks, a call to takeForks will remain pending until both other functions are called, too. The same holds for calls to leftFork or rightFork: only after all three functions are called is the function body executed, returning control to takeForks's caller. The order in which the functions are called is not important and is in no way related to the order in which the functions appear in the def statement.

The order of appearance in the def statement has a different effect, though: While it is possible to specify explicitly which of the listed functions are supposed to return (e.g. with returnto.takeForks()), the shorthand return() refers always to the rightmost function in the list.

In fact, return is just an automatically generated function of type Unit --> Void (because Unit} is the return type of takeForks) that can be used like any other function, and returnto is nothing but a record of such functions labeled with appropriate names.

A call to releaseForks returns in any case, but produces calls to leftFork and rightFork in parallel to returning control.

Function Symbols are First-Class Values

So far, the code is concerned with only one philosopher. What remains to do is to differentiate between those items that are specific to one philosopher and those that are shared (i.e. the forks):

new initPhilosopher: (Unit --> Void, Unit --> Void, String) --> Void;

def initPhilosopher(leftFork, rightFork, name)
{
    new takeForks: Unit --> Unit;
    new releaseForks: Unit --> Unit;
    
    def takeForks() & leftFork() & rightFork(): return();
    def releaseForks(): leftFork() & rightFork() & return();
    
    ...
}

The language feature used here is that function symbols are first-class values: they can be given arbitrary local identifiers, they can be passed as parameters to function invocations and function bodies can return function symbols just like any string or integer. Furthermore, function bodies need not be defined together with function symbols in the same syntactic block. Instead, new function bodies may also be attached to function symbols that were passed as parameters or returned from a function invocation.

Now, leftFork and rightFork refer to arguments passed to initPhilosopher. This way, the same forks can be passed to several philosophers, each of which in turn adds an additional function body that synchronizes with that philosopher's takeForks function. In parallel, initial calls must be made to the individual forks so they can be picked up by one of the philosphers:

new forkA: Unit --> Void;
new forkB: Unit --> Void;
new forkC: Unit --> Void;
new forkD: Unit --> Void;

forkA() & forkB() & forkC() & forkD() &

initPhilosopher(forkA, forkB, "Descartes") &
initPhilosopher(forkB, forkC, "Sokrates") &
initPhilosopher(forkC, forkD, "Sartre") &
initPhilosopher(forkD, forkA, "Kant");

The calls to forkX and initPhilosopher are delimited by the &-operator, which causes these statements to be executed in parallel.

Putting all these pieces together yields the code displayed at the top of this page. As already mentioned above, the solution developed here has some desirable properties that are not as easily achieved using traditional synchronization primitives.