Prev: 2nd call - INFORMATICS 2010: submissions until 31 May 2010
Next: OO Textbook Using C#
From: raould on 24 May 2010 17:47
cqs seems to help with referential transparency. but it doesn't
inherently help with races. whereas an 'atomic' compare-and-set lets
you not have to externally synchronize, as it were. darned if you do,
darned if you don't. any preferences about which is less evil?
From: S Perryman on 25 May 2010 05:06
raould wrote:

> cqs seems to help with referential transparency. but it doesn't
> inherently help with races. whereas an 'atomic' compare-and-set lets
> you not have to externally synchronize, as it were. darned if you do,
> darned if you don't. any preferences about which is less evil?

Look at the "SCOOP" stuff associated with Eiffel.

Pre-conditions become synchronising conditions.
If you cannot synchronise (conditions are false) , you are blocked.

A classic example :

type DataPipe<E>
{
boolean empty() ;
boolean full() ;

invariant : NOT(empty AND full)

insert(E) ;
pre: NOT(full)
post: NOT(empty)

E remove() ;
pre: NOT(empty)
}


The producer (the insert op) has the same pre-conditions as would be the
case for (correctness in) a sequential system. But if the pipe is full,
in a concurrent system the producer is blocked. At some future time, the
producer will become active again, the pre-condition holds, and the
producer gets access to the pipe.

Similarly for a consumer (the remove op) .


See below for the basic template for this approach.


Regards,
Steven Perryman

------------------------------------------


executing = true ;
while executing
do
M = mutual exclusion on resource R ;
// If you cannot get M, you are blocked

// Only evaluate those pre-conditions needed for concurrency control
bool pre = FORALL e IN pre-condition(R, op, "sync" ) : e(R, ...)

if pre
do
R.op(...) ;
executing = false ;
end

release M ;

// You cannot do anything so give up execution resources to others
if executing do yield end
end
 | 
Pages: 1
Prev: 2nd call - INFORMATICS 2010: submissions until 31 May 2010
Next: OO Textbook Using C#