Eiffel SCOOP: a typical example

The following is a routine, written in ordinary Eiffel without concurrency, to transfer a certain amount of money from an account to another:

transfer (amount: INTEGER ; source, target: ACCOUNT)
		-- Transfer amount dollars from source to target.
	require
		amount_positive: amount> 0
		enough: source·balance >= amount
	do
		source·withdraw (amount)
		target·deposit (amount)
	ensure
		removed: source·balance = old source·balance – amount
		added: target·balance = old target·balance + amount
	end

The body (do …) describes the implementation: withdraw the amount from the source, deposit it on the target. The precondition (require …) describes the condition for applicability: there must be enough money on the source. The postcondition (ensure…) expresses the expected final state: the amount has been removed from the balance of the source and added to the balance of the target.

How do we turn such a routine into a concurrent operation? The problem is that if several such operations are proceeding in parallel we cannot allow arbitrary interleaving. For example two transfer operations for $800 could both find that the precondition is satisfied on the source, as it has a balance of $1000; then they would both proceed to transfer $800 to different targets, but this is wrong as there was not enough money to allow both!

In usual approaches to concurrent programming, programmers have to write complicated synchronization operations to guarantee that certain instructions are executed together. Here, for example, the precondition checking, the withdraw and the deposit should never be interleaved with instructions from another instance of transfer. In addition, if the source account does not initially have a high enough balance, the operation should wait. All this leads to tedious, low-level and error-prone programming and, as noted, to programs that are very hard to debug.

With Eiffel and SCOOP the transition to concurrency is straightforward. All that has to change in the above non-concurrent code, to make it concurrent but still correct and safe, is the header of the routine:

transfer (amount: INTEGER ; source, target: separate ACCOUNT)
		-- Transfer amount dollars from source to target.
	... All the rest as before! ...

Declaring the accounts as separate tells the compiler that they are going to be handled by concurrent threads. All scheduling needs – including waiting on a source account whose balance is too small, as expressed by the precondition – are taken care of entirely by the SCOOP scheduler.

How do I get SCOOP?

SCOOP is available for download as part of EiffelStudio. For a more in-depth presentation, read the SCOOP section in the Eiffel Documentation or watch the SCOOP video.