To appear in the Proceedings of CONCUR, August 2005.
finish
operation that detects termination
of activities. Atomicity is obtained through the use of atomic
blocks. Activities may repeatedly detect quiescence of a
data-dependent collection of (distributed) activities through a notion
of clocks, generalizing barriers. Thus X10 has a handful of
orthogonal constructs for space, time,
sequencing and atomicity. X10 smoothly combines and
generalizes the current dominant paradigms for shared memory computing
and message passing.
We present a bisimulation-based operational semantics for X10 building on the formal semantics for ``Middleweight Java''. We establish the central theorem of X10: programs without conditional atomic blocks do not deadlock.