Information Technology Reference
In-Depth Information
synchronize inference rules. The labels allow an external observer to follow the tran-
sitions. Our semantics is a pure reduction semantics without labels because we do not
require observable transitions.
Cenciarelli, Knapp, Reus, and Wirsing [6] also describe an operational semantics for
a larger subset of multi-threaded Java. They cover a larger number of multi-threaded
aspects than [1]. In particular they formalize Java's notification mechanism and the
working memory. A configuration consists of a function that maps each thread to its
expression and its local environments. The configuration also has a container with the
objects and the static typing information. Lastly, the configuration consists of an event
space. The event space is a partially ordered set of events that have been executed by the
threads. The ordering reflects the order in which the events took place. An event space
serves two purposes. First, it contains certain aspects of the state. For example, the lock
and unlock actions tell us which thread owns which lock. Second, it records the history.
A number of constraints state when an event space is valid. Hence, the event space
indicates which further actions can take place. The authors use two different validity
constraints for both Java's non-prescient semantics and its prescient semantics. Using
this, they show that any prescient execution of a properly synchronized program can be
simulated by a non-prescient execution. Compared to our semantics, there is no clean
division between program text and the state and there is no clean division between the
state and the typing information.
Lochbihler [19] suggest a different operational semantics for a large subset of
multi-threaded Java. Just like [6], he covers the notification mechanism, but he does
not formalize the working memory. He defines an instantiating semantics based on an
extension of Jinja [17]. Jinja is an operational semantics for a subset of single-threaded
Java. The instantiating semantics is used for the sequential case. Lochbihler defines a
generic formal framework to lift the instantiating semantics to the concurrent case. The
configuration of the instantiating semantics consists of the expression, a container with
the objects, and the local environments. The state of the framework semantics consists
of the lock status, the thread information with the thread's expression along with the
thread's local environments, a container with the objects, and the wait sets. Lochbihler
formalizes the notion of deadlocks, where deadlocks are either based on locks or on
wait sets. He then proves that every program that satisfies certain criteria either pro-
duces a final value, throws an exception, or deadlocks. He also shows that every such
program preserves type safety.
3
Language Overview
SCOOP is a programming language based on Eiffel, an object-oriented programming
language, defined in the Eiffel ECMA standard [9]. SCOOP's concurrency model can
be applied to other programming languages as well. For this reason, this work does not
focus on SCOOP, but on its concurrency model. This section defines a subset of SCOOP,
reduced to the parts that are relevant for the concurrency model. It presents the syntax
of the subset and a list of simplifications. It then discusses the program representation
that this formalization assumes.
 
Search WWH ::




Custom Search