Information Technology Reference
In-Depth Information
when the procedure starts executing. The task specification can define a number of en-
try points with parameters; an entry point specifies an action the task can synchronize
on. An accept statement within the task body indicates the point where the rendezvous
can take place. Another task calls the entry point to take part in the rendezvous. With
a select statement, one can wait for multiple entry points; alternatives may be guarded
with boolean expressions. Ada defines protected objects - a monitor-like construct with
guards instead of conditional variables. A protected object is declared within a proce-
dure; it has a specification and an implementation.
The occam programming language [32] builds on the CSP process algebra [13]. A
parallel construct defines a number of processes that execute concurrently; the parallel
construct terminates when all spawned processes terminated. Processes communicate
with each other through named channels. The alternation construct defines a number of
processes, where only one of them gets executed; a guard defines when a process can
be executed.
X10 [7], Fortress [2], and Chapel [15] are based on the Partitioned Global Ad-
dress Space (PGAS) model. PGAS uses a global shared memory. It defines portions
on the global shared memory and associates them to specific processors to improve
performance and scalability. X10 provides important abstractions such as places, asyn-
chronous methods, future invocations, and barriers. However, it places a considerable
burden on programmers. Fortress offers implicit parallelization of loops and operations
on data structures. Chapel provides a higher-level multithreaded parallel programming
model with abstractions for data parallelism, task parallelism, and nested parallelism.
Linda [12] is a coordination language to connect concurrent components; the com-
ponents can be written in different programming languages. The coordination is based
on a tuple space, which holds data tuples that can be stored and retrieved by the pro-
cesses. Pattern matching is used to read and remove tuples; the operations block until a
matching tuple is found. The eval construct creates a new process to evaluate an expres-
sion; the new process writes the evaluation result into the tuple space. Implementations
of Linda can be found in several programming languages such as Java and C.
For the related languages mentioned above, we are not aware of rigorous behav-
ioral specifications, with the exception of C
and occam, which use the Join Calculus
respectively CSP as the underlying model. For multi-threaded Java however, such for-
malizations have been attempted.
Abraham, de Boer, de Roever, and Steffen [1] present an operational semantics for a
subset of multi-threaded Java. They focus on the most important multi-threaded aspects,
i.e., dynamic thread creation, thread termination, and re-entrant monitors. The seman-
tics consists of two components: the semantics for isolated objects and the semantics
for interacting objects. The authors want to use the semantics to develop a proof sys-
tem that is based on an existing proof-system for isolated objects. A configuration is a
set of instance configurations. An instance configuration contains the attribute values
of one object. It also contains the local environment and the expression of each thread
that is concurrently executing within the object. In modeling the state of a program,
our semantics strictly separates the actions to be executed from the data. This makes
it easier to derive implementations from the semantics because an implementation is
likely to keep the program text and data separate. Abraham et al. use transition labels to
ω
 
Search WWH ::




Custom Search