/** Semaphore Example : Mutual Exclusion / Synchronization in DLP

Mutual Exclusion / Synchronization in DLP

Introduction

The core language of DLP [Eliens] is similar to Prolog [Bratko], [Clocksin], [Online] : logical variables, unification, and backtracking are the basic language characteristics of DLP. In addition to these Prolog-like language constructs, the language supports multi-threaded objects, non-logical object variables and conditional communication by rendez-vous. As an illustration, this overview shows how a (binary) semaphore may be implemented by means of a (conditional) rendez-vous in DLP. Although the implemention of a lower-level synchronization primitive by means of a higher-level one is rather straightforward, it illustrates several ways a rendez-vous may be used to express synchronization between active objects. For a slightly more complex example of multi-threaded objects and the rendez-vous take a look at the active bounded buffer source code.

Mutual Exclusion / Synchronization

Multi-threaded objects require some sort of mutual exclusion in order to keep their internal state consistent : active objects that are allowed to access a common resource without mutual exclusion, may leave the resource in an inconsistent state. Many mutual exclusion and synchronization mechanisms have been designed and their abstraction level is illustrated by the way they solve a number of classical mutual exclusion problems, e.g. the bounded buffer, readers - writers, and dining philosophers problems. A so called (binary) semaphore is one of the lowest-level mechanisms of all known mutual exclusion concepts. Examples of mechanisms at a higher-level (than a binary semaphore) are condition variables (wait / signal, wait / notify), critical regions, monitors, Ada's rendez-vous, and blocking message passing [Andrews], [Ben-Ari].
Higher-level synchronization techniques are implemented by means of lower-level mechanisms. As mentioned, lower-level concepts may be implemented by higher-level constructs in a straightforward way : their implementation often looks somewhat artificial as is the case in the example below.

The (binary) semaphore concept is based on railroad signposts and consists of two operations : lock and unlock. We prefer the names lock and unlock because they're close to the POSIX Threads terminology (pthread_mutex_lock, pthread_mutex_trylock, pthread_mutex_unlock); they express in a more intuitive way what the operations actually do. Originally semaphore operations, as proposed by [Dijkstra], were called "p" and "v" (Dutch for : passeren / vrijgeven). As shown in the pseudo code below, the lock and unlock primitives delimit a critical piece of code for which mutual exclusion is required : 
	....
	sema <- lock
	/* critical */
	sema <- unlock
	....
The invocation of a lock operation will block the invoking thread in case another thread has already executed the lock operation of the corresponding semaphore, otherwise the current thread is allowed to continue its execution immediately. After acquiring the lock, a thread has exclusive access to the code fragment denoted as "critical". When the critical work is done, a thread executes the corresponding unlock operation : this will unblock one of the (possibly many) other threads that are waiting as the result of their own lock invocation.

Conditional Rendez-vous


A (conditional) rendez-vous in DLP is expressed by means of a so called accept statement. An accept statement specifies a disjunction of one or more accept expressions : 
	AcceptStatement ::=
		accept(AcceptExpression1, .... , AcceptExpressionN)
A single accept expression defines a method that an object is willing to accept. In addition, an accept expression allows for the specification of a conjunction of conditions and / or the actual code of the method : 
	AcceptExpresssion ::=
		AcceptMethod						[AE.1]
	or	AcceptMethod ==> MethodBody				[AE.2]
	or	AcceptMethod <== [ MethodGuard ]			[AE.3]
	or	AcceptMethod <== [ MethodGuard ] ==> MethodBody		[AE.4]
	;;
In AcceptExpression [AE.1] and [AE.3], the AcceptMethod should be a callable method. In [AE.2] and [AE.4], the code of AcceptMethod is specified in the MethodBody, i.e. there is no explicit AcceptMethod method called in the current object hierarchy. An AcceptMethod and MethodGuard have one of the following forms : 
	AcceptMethod ::=
		method
	or	method(Arg1, ..., ArgN)
	;;

	MethodGuard ::=
		Condition
	or	Condition1, ..., ConditionN
	;;
A method invocation like "Obj <- method(...)" will be accepted by an active object "Obj" when both "method(...)" unifies with one of the AcceptMethod entries of the accept statement in "Obj" and the (optional) corresponding MethodGuard holds.
In case a particular method has been accepted (a rendez-vous has taken place), other threads that are invoking a method concurrently, will be blocked until the previously accepted method has delivered its (first) solution. After returning its solution, other method calls may be accepted, depending on the specified accept expressions in the accept statement of "Obj".

References

Example

Object semaphore1 below has three methods : lock, unlock, and the active object constructor semaphore1. The first accept statement, accept(lock), states that object semaphore1 is only willing to accept a lock method call. When such a call is accepted other threads will block in case they invoke a lock concurrently. After accept(lock) object semaphore1 only accepts an unlock as expressed by the accept(unlock) statement. A thread for which lock is accepted will be able to continue its execution, in particular it will be able to execute its "critical" section of code. When this code has been executed, a call to unlock will unblock one of the other threads that are waiting for the acceptance of their lock operation.

It should be clear by now why a binary semaphore is called a lower-level synchronization concept. Apart from the fact that a semaphore has no facilities for expressing additional synchronization conditions, a binary semaphore is error-prone : the lock and unlock invocations should always be carefully combined as illustrated in the worker object. 
**/

:-object semaphore1.

	lock.
	unlock.

	semaphore1 :-
		repeat,
			accept(lock),
			accept(unlock),
		fail.

:-end_object semaphore1.

/**
Object semaphore2 introduces the notion of state : non-logical variable "n" denotes whether a lock has already been acquired by a particular thread. The guards "[ n > 0 ]" and "[ n >= 0 ]" provide for the conditions under which the methods lock and unlock will be accepted. 
**/

:-object semaphore2.

	var n = 1.

	lock :-  -- n .
	unlock :- ++ n .

	semaphore2 :-
		repeat,
			accept(
				lock <== [ n > 0 ],
				unlock <== [ n >= 0 ]
			),
		fail.

:-end_object semaphore2.

/**
Object semaphore3 extends semaphore2 : the actual code of the lock and unlock operations is moved to the MethodBody part of the corresponding AcceptExpressions. 
**/

:-object semaphore3.

	var n = 1.

	semaphore3 :-
		repeat,
			accept(
				lock <== [ n > 0 ] ==> -- n,
				unlock <== [ n >= 0 ] ==> ++ n
			),
		fail.

:-end_object semaphore3.

/**
Object critical ... 
**/

:-object critical.

	var counter = 0.

	work(ThisWorker, Msecs) :-
		++ counter,
		format('~w~t: counter = ~w (block ~w msecs)~n', [ThisWorker, counter, Msecs]),
		sleep(Msecs).

:-end_object critical.


/***
Object worker ... 
***/

:-object worker.

	var todo = 0.

	worker(ToDo, Sema, Msecs) :-
		todo := ToDo,
		loop(Sema, Msecs),
		format('end of ~w~n', [this]).

	loop(Sema, Msecs) :-
		repeat,
			Sema <- lock,
			critical <- work(this, Msecs),
			Sema <- unlock,
			-- todo,
		todo < 1,
		!.

:-end_object worker.

/**
Remove the text_area / 1 and set_output / 1 calls below in case you would like to run the example as a stand-alone program, i.e. not as an applet in a browser. Note that the text in this html file is actually comment in a DLP program : save it in e.g. pxsema.pl and compile / execute the program. 
**/

:-object pxsema.

	main :-
		text_area(BrowserStream),	%% only required for execution
		set_output(BrowserStream),	%% in a browser

		%% PV := new(semaphore1),
		%% PV := new(semaphore2),
		PV := new(semaphore3),
		_W0 := new(worker(5, PV, 800)),
		_W1 := new(worker(5, PV, 400)),
		_W2 := new(worker(5, PV, 200)),
		format('end of ~w~n', [this]).

:-end_object pxsema.

/**
**/