Search

Concurrent abstraction layers are ubiquitous in modern computer systems because of the pervasiveness of multithreaded programming and multicore hardware. Abstraction layers are used to hide the implementation details (e.g., fine-grained synchronization) and reduce the complex dependencies among components at different levels of abstraction. Despite their obvious importance, concurrent abstraction layers have not been treated formally. This severely limits the applicability of layer-based techniques and makes it difficult to scale verification across multiple concurrent layers. In this paper, we present CCAL---a fully mechanized programming toolkit developed under the CertiKOS project---for specifying, composing, compiling, and linking certified concurrent abstraction layers. CCAL consists of three technical novelties: a new game-theoretical, strategy-based compositional semantic model for concurrency (and its associated program verifiers), a set of formal linking theorems for composing multithreaded and multicore concurrent layers, and a new CompCertX compiler that supports certified thread-safe compilation and linking. The CCAL toolkit is implemented in Coq and supports layered concurrent programming in both C and assembly. It has been successfully applied to build a fully certified concurrent OS kernel with fine-grained locking.

We present nesC, a programming language for networked embedded systems that represent a new design space for application developers. An example of a networked embedded system is a sensor network, which consists of (potentially) thousands of tiny, lowpower "motes," each of which execute concurrent, reactive programs that must operate with severe memory and power constraints. nesC's contribution is to support the special needs of this domain by exposing a programming model that incorporates event-driven execution, a flexible concurrency model, and component-oriented application design. Restrictions on the programming model allow the nesC compiler to perform whole-program analyses, including data-race detection (which improves reliability) and aggressive function inlining (which reduces resource consumption). nesC has been used to implement TinyOS, a small operating system for sensor networks, as well as several significant sensor applications. nesC and TinyOS have been adopted by a large number of sensor network research groups, and our experience and evaluation of the language shows that it is effective at supporting the complex, concurrent programming style demanded by this new class of deeply networked systems.

Managed languages typically use read barriers to interpret forwarding pointers introduced to keep track of copied objects. For example, in a multicore environment with thread-local heaps and a global, shared heap, an object initially allocated on a local heap may be copied to a shared heap if it becomes the source of a store operation whose target location resides on the shared heap. As part of the copy operation, a forwarding pointer may be established in the original object to point to the copied object. This level of indirection avoids the need to update all of the references to the object that has been copied. In this paper, we consider the design of a managed runtime that eliminates read barriers. Our design is premised on the availability of a sufficient degree of concurrency to stall operations that would otherwise necessitate the copy. Stalled actions are deferred until the next local collection, avoiding exposing forwarding pointers to the mutator. In certain important cases, procrastination is unnecessary -- lightweight runtime techniques can sometimes be used to allow objects to be eagerly copied when their set of incoming references is known, or when it can be determined that having multiple copies would not violate program semantics. We evaluate our techniques on 3 platforms: a 16-core AMD64 machine, a 48-core Intel SCC, and an 864-core Azul Vega 3. Experimental results over a range of parallel benchmarks indicate that our approach leads to notable performance gains (20 - 32% on average) without incurring any additional complexity.

Many concurrent programming models enable both transactional memory and message passing. For such models, researchers have built increasingly efficient implementations and defined reasonable correctness criteria, while it remains an open problem to obtain the best of both worlds. We present a programming model that is the first to have opaque transactions, safe asynchronous message passing, and an efficient implementation. Our semantics uses tentative message passing and keeps track of dependencies to enable undo of message passing in case a transaction aborts. We can program communication idioms such as barrier and rendezvous that do not deadlock when used in an atomic block. Our experiments show that our model adds little overhead to pure transactions, and that it is significantly more efficient than Transactional Events. We use a novel definition of safe message passing that may be of independent interest.

Fine-grained concurrent data structures are crucial for gaining performance from multiprocessing, but their design is a subtle art. Recent literature has made large strides in verifying these data structures, using either atomicity refinement or separation logic with rely-guarantee reasoning. In this paper we show how the ownership discipline of separation logic can be used to enable atomicity refinement, and we develop a new rely-guarantee method that is localized to the definition of a data structure. We present the first semantics of separation logic that is sensitive to atomicity, and show how to control this sensitivity through ownership. The result is a logic that enables compositional reasoning about atomicity and interference, even for programs that use fine-grained synchronization and dynamic memory allocation.

Building applications that are responsive and can exploit parallel hardware while remaining simple to write, understand, test, and maintain, poses an important challenge for developers. In particular, it is often desirable to enable various tasks to read or modify shared data concurrently without requiring complicated locking schemes that may throttle concurrency and introduce bugs. We introduce a mechanism that simplifies the parallel execution of different application tasks. Programmers declare what data they wish to share between tasks by using isolation types, and execute tasks concurrently by forking and joining revisions . These revisions are isolated: they read and modify their own private copy of the shared data only. A runtime creates and merges copies automatically, and resolves conflicts deterministically, in a manner declared by the chosen isolation type. To demonstrate the practical viability of our approach, we developed an efficient algorithm and an implementation in the form of a C# library, and used it to parallelize an interactive game application. Our results show that the parallelized game, while simple and very similar to the original sequential game, achieves satisfactory speedups on a multicore processor.

While many type systems based on the intuitionistic fragment of linear logic have been proposed, applications in programming languages of the full power of linear logic - including double-negation elimination - have remained elusive. Meanwhile, linearity has been used in many type systems for concurrent programs - e.g., session types - which suggests applicability to the problems of concurrent programming, but the ways in which linearity has interacted with concurrency primitives in lambda calculi have remained somewhat ad-hoc. In this paper we connect classical linear logic and concurrent functional programming in the language Lolliproc, which provides simple primitives for concurrency that have a direct logical interpretation and that combine to provide the functionality of session types. Lolliproc features a simple process calculus "under the hood" but hides the machinery of processes from programmers. We illustrate Lolliproc by example and prove soundness, strong normalization, and confluence results, which, among other things, guarantees freedom from deadlocks and race conditions.

The most intuitive memory model for shared-memory multithreaded programming is sequential consistency (SC), but it disallows the use of many compiler and hardware optimizations thereby impacting performance. Data-race-free (DRF) models, such as the proposed C++0x memory model, guarantee SC execution for datarace-free programs. But these models provide no guarantee at all for racy programs, compromising the safety and debuggability of such programs. To address the safety issue, the Java memory model, which is also based on the DRF model, provides a weak semantics for racy executions. However, this semantics is subtle and complex, making it difficult for programmers to reason about their programs and for compiler writers to ensure the correctness of compiler optimizations. We present the DRFx memory model, which is simple for programmers to understand and use while still supporting many common optimizations. We introduce a memory model (MM) exception which can be signaled to halt execution. If a program executes without throwing this exception, then DRFx guarantees that the execution is SC. If a program throws an MM exception during an execution, then DRFx guarantees that the program has a data race. We observe that SC violations can be detected in hardware through a lightweight form of conflict detection. Furthermore, our model safely allows aggressive compiler and hardware optimizations within compiler-designated program regions. We formalize our memory model, prove several properties about this model, describe a compiler and hardware design suitable for DRFx, and evaluate the performance overhead due to our compiler and hardware requirements.

As concurrent programming becomes prevalent, software providers are investing in concurrency libraries to improve programmer productivity. Concurrency libraries improve productivity by hiding error-prone, low-level synchronization from programmers and providing higher-level concurrent abstractions. Testing such libraries is difficult, however, because concurrency failures often manifest only under particular scheduling circumstances. Current best testing practices are often inadequate: heuristic-guided fuzzing is not systematic, systematic schedule enumeration does not find bugs quickly, and stress testing is neither systematic nor fast. To address these shortcomings, we propose a prioritized search technique called GAMBIT that combines the speed benefits of heuristic-guided fuzzing with the soundness, progress, and reproducibility guarantees of stateless model checking. GAMBIT combines known techniques such as partial-order reduction and preemption-bounding with a generalized best-first search frame- work that prioritizes schedules likely to expose bugs. We evaluate GAMBIT's effectiveness on newly released concurrency libraries for Microsoft's .NET framework. Our experiments show that GAMBIT finds bugs more quickly than prior stateless model checking techniques without compromising coverage guarantees or reproducibility.

Exploiting the emerging reality of affordable multi-core architectures goes through providing programmers with simple abstractions that would enable them to easily turn their sequential programs into concurrent ones that expose as much parallelism as possible. While transactional memory promises to make concurrent programming easy to a wide programmer community, current implementations either disallow nested transactions to run in parallel or do not scale to arbitrary parallel nesting depths. This is an important obstacle to the central goal of transactional memory, as programmers can only start parallel threads in restricted parts of their code. This paper addresses the intrinsic difficulty behind the support for parallel nesting in transactional memory, and proposes a novel solution that, to the best of our knowledge, is the first practical solution to meet the lowest theoretical upper bound known for the problem. Using a synthetic workload configured to test parallel transactions on a multi-core machine, a practical implementation of our algorithm yields substantial speed-ups (up to 22x with 33 threads) relatively to serial nesting, and shows that the time to start and commit transactions, as well as to detect conflicts, is independent of nesting depth.

Concurrent programming errors arise when threads share data incorrectly. Programmers often avoid these errors by using synchronization to enforce a simple ownership policy: data is either owned exclusively by a thread that can read or write the data, or it is read owned by a set of threads that can read but not write the data. Unfortunately, incorrect synchronization often fails to enforce these policies and memory errors in languages like C and C++ can violate these policies even when synchronization is correct. In this paper, we present a dynamic analysis for checking ownership policies in concurrent C and C++ programs despite memory errors. The analysis can be used to find errors in commodity multi-threaded programs and to prevent attacks that exploit these errors. We require programmers to write ownership assertions that describe the sharing policies used by different parts of the program. These policies may change over time, as may the policies' means of enforcement, whether it be locks, barriers, thread joins, etc. Our compiler inserts checks in the program that signal an error if these policies are violated at runtime. We evaluated our tool on several benchmark programs. The run-time overhead was reasonable: between 0 and 49% with an average of 26%. We also found the tool easy to use: the total number of ownership assertions is small, and the asserted specification and implementation can be debugged together by running the instrumented program and addressing the errors that arise. Our approach enjoys a pleasing modular soundness property: if a thread executes a sequence of statements on variables it owns, the statements are serializable within a valid execution, and thus their effects can be reasoned about in isolation from other threads in the program.

In Concurrent ML, synchronization abstractions can be defined and passed as values, much like functions in ML. This mechanism admits a powerful, modular style of concurrent programming, called higher-order concurrent programming . Unfortunately, it is not clear whether this style of programming is possible in languages such as Concurrent Haskell, that support only first-order message passing. Indeed, the implementation of synchronization abstractions in Concurrent ML relies on fairly low-level, language-specific details. In this paper we show, constructively, that synchronization abstractions can be supported in a language that supports only first-order message passing. Specifically, we implement a library that makes Concurrent ML-style programming possible in Concurrent Haskell. We begin with a core, formal implementation of synchronization abstractions in the π-calculus. Then, we extend this implementation to encode all of Concurrent ML's concurrency primitives (and more!) in Concurrent Haskell. Our implementation is surprisingly efficient, even without possible optimizations. In several small, informal experiments, our library seems to outperform OCaml's standard library of Concurrent ML-style primitives. At the heart of our implementation is a new distributed synchronization protocol that we prove correct. Unlike several previous translations of synchronization abstractions in concurrent languages, we remain faithful to the standard semantics for Concurrent ML's concurrency primitives. For example, we retain the symmetry of choose, which can express selective communication. As a corollary, we establish that implementing selective communication on distributed machines is no harder than implementing first-order message passing on such machines.

Memoization is a well-known optimization technique used to eliminate redundant calls for pure functions. If a call to a function f with argument v yields result r, a subsequent call to f with v can be immediately reduced to r without the need to re-evaluate f's body. Understanding memoization in the presence of concurrency and communication is significantly more challenging. For example, if f communicates with other threads, it is not sufficient to simply record its input/output behavior; we must also track inter-thread dependencies induced by these communication actions. Subsequent calls to f can be elided only if we can identify an interleaving of actions from these call-sites that lead to states in which these dependencies are satisfied. Similar issues arise if f spawns additional threads. In this paper, we consider the memoization problem for a higher-order concurrent language whose threads may communicate through synchronous message-based communication. To avoid the need to perform unbounded state space search that may be necessary to determine if all communication dependencies manifest in an earlier call can be satisfied in a later one, we introduce a weaker notion of memoization called partial memoization that gives implementations the freedom to avoid performing some part, if not all, of a previously memoized call. To validate the effectiveness of our ideas, we consider the benefits of memoization for reducing the overhead of recomputation for streaming, server-based, and transactional applications executed on a multi-core machine. We show that on a variety of workloads, memoization can lead to substantial performance improvements without incurring high memory costs.

Deadlock in multithreaded programs is an increasingly important problem as ubiquitous multicore architectures force parallelization upon an ever wider range of software. This paper presents a theoretical foundation for dynamic deadlock avoidance in concurrent programs that employ conventional mutual exclusion and synchronization primitives (e.g., multithreaded C/Pthreads programs). Beginning with control flow graphs extracted from program source code, we construct a formal model of the program and then apply Discrete Control Theory to automatically synthesize deadlock-avoidance control logic that is implemented by program instrumentation. At run time, the control logic avoids deadlocks by postponing lock acquisitions. Discrete Control Theory guarantees that the program instrumented with our synthesized control logic cannot deadlock. Our method furthermore guarantees that the control logic is maximally permissive: it postpones lock acquisitions only when necessary to prevent deadlocks, and therefore permits maximal runtime concurrency. Our prototype for C/Pthreads scales to real software including Apache, OpenLDAP, and two kinds of benchmarks, automatically avoiding both injected and naturally occurring deadlocks while imposing modest runtime overheads.

Undergraduate computer science students typically have only a limited understanding of their favorite languages and no inkling of other programming paradigms. Yet modern programmers typically work with several languages, and the availability of cheap concurrency is exposing fundamental problems in standard concurrent programming techniques (mutable objects and threads). This situation presents a great opportunity: by exploring nonstandard techniques for gaining intellectual control over concurrent programs, one can motivate and teach important semantic concepts (such as scoping) and important programming concepts (such as functional abstraction). Such a curriculum stimulates student interest in exploring new programming paradigms.

Software Transactional Memory (STM) is an attractive basis for the development of language features for concurrent programming. However, the semantics of these features can be delicate and problematic. In this paper we explore the tradeoffs between semantic simplicity, the viability of efficient implementation strategies, and the flexibilityof language constructs. Specifically, we develop semantics and type systems for the constructs of the Automatic Mutual Exclusion (AME) programming model; our results apply also to other constructs, such as atomic blocks. With this semantics as a point of reference, we study several implementation strategies. We model STM systems that use in-place update, optimistic concurrency, lazy conflict detection, and roll-back. These strategies are correct only under non-trivial assumptions that we identify and analyze. One important source of errors is that some efficient implementations create dangerous 'zombie' computations where a transaction keeps running after experiencing a conflict; the assumptions confine the effects of these computations.

We present the TIC (Transactions with Isolation and Cooperation) model for concurrent programming. TIC adds to standard transactional memory the ability for a transaction to observe the effects of other threads at selected points. This allows transactions to cooperate, as well as to invoke nonrepeatable or irreversible operations, such as I/O. Cooperating transactions run the danger of exposing intermediate state and of having other threads change the transaction's state. The TIC model protects against unanticipated interference by having the type system keep track of all operations that may (transitively) violate the atomicity of a transaction and require the programmer to establish consistency at appropriate points. The result is a programming model that is both general and simple. We have used the TIC model to re-engineer existing lock-based applications including a substantial multi-threaded web mail server and a memory allocator with coarse-grained locking. Our experience confirms the features of the TIC model: It is convenient for the programmer, while maintaining the benefits of transactional memory.

We present the first shape analysis for multithreaded programs that avoids the explicit enumeration of execution-interleavings. Our approach is to automatically infer a resource invariant associated with each lock that describes the part of the heap protected by the lock. This allows us to use a sequential shape analysis on each thread. We show that resource invariants of a certain class can be characterized as least fixed points and computed via repeated applications of shape analysis only on each individual thread. Based on this approach, we have implemented a thread-modular shape analysis tool and applied it to concurrent heap-manipulating code from Windows device drivers.

Concurrent programs require high-level abstractions in order to manage complexity and enable compositional reasoning. In this paper, we introduce a novel concurrency abstraction, dubbedtransactional events, which combines first-class synchronous message passing events with all-or-nothing transactions. This combination enables simple solutions to interesting problems in concurrent programming. For example, guarded synchronous receive can be implemented as an abstract transactional event, whereas in other languages it requires a non-abstract, non-modular protocol. As another example, three-way rendezvous can be implemented as an abstract transactional event, which is impossible using first-class events alone. Both solutions are easy to code and easy to reason about.The expressive power of transactional events arises from a sequencing combinator whose semantics enforces an all-or-nothing transactional property – either both of the constituent events synchronize in sequence or neither of them synchronizes. This sequencing combinator, along with a non-deterministic choice combinator, gives transactional events the compositional structure of a monad-with-plus. We provide a formal semantics for transactional events and give a detailed account of an implementation.

Programmers have traditionally used locks to synchronize concurrent access to shared data. Lock-based synchronization, however, has well-known pitfalls: using locks for fine-grain synchronization and composing code that already uses locks are both difficult and prone to deadlock. Transactional memory provides an alternate concurrency control mechanism that avoids these pitfalls and significantly eases concurrent programming. Transactional memory language constructs have recently been proposed as extensions to existing languages or included in new concurrent language specifications, opening the door for new compiler optimizations that target the overheads of transactional memory.This paper presents compiler and runtime optimizations for transactional memory language constructs. We present a high-performance software transactional memory system (STM) integrated into a managed runtime environment. Our system efficiently implements nested transactions that support both composition of transactions and partial roll back. Our JIT compiler is the first to optimize the overheads of STM, and we show novel techniques for enabling JIT optimizations on STM operations. We measure the performance of our optimizations on a 16-way SMP running multi-threaded transactional workloads. Our results show that these techniques enable transactional memory's performance to compete with that of well-tuned synchronization.

The feasibility and efficiency of analyzing concurrent programs mostly relies on the programs' representations. So modeling concurrent programs in a proper and suitable way is very important. Protected objects, which have been introduced in Ada95, are of significant importance in concurrent programming language. In this paper, process algebra is used to model Ada95 protected objects in a neat and tidy way. Because using process algebra can simplify process composition and conveniently hide internal details, it becomes easy to analyze Ada concurrent programs with protected objects and to combat problems of state explosion. In addition, many mechanisms similar to protected objects can be modeled in this way. With these models, many analyses, such as model checking, can be performed.

Concurrent programming is notoriously difficult. Current abstractions are intricate and make it hard to design computer systems that are reliable and scalable. We argue that these problems can be addressed by moving to a declarative style of concurrency control in which programmers directly indicate the safety properties that they require. In our scheme the programmer demarks sections of code which execute within lightweight software-based transactions that commit atomically and exactly once. These transactions can update shared data, instantiate objects, invoke library features and so on. They can also block, waiting for arbitrary boolean conditions to become true. Transactions which do not access the same shared memory locations can commit concurrently. Furthermore, in general, no performance penalty is incurred for memory accesses outside transactions.We present a detailed design of this proposal along with an implementation and evaluation. We argue that the resulting system ( i ) is easier for mainstream programmers to use, ( ii ) prevents lock-based priority-inversion and deadlock problems and ( iii ) can offer performance advantages.

The mostly concurrent garbage collection was presented in the seminal paper of Boehm et al. With the deployment of Java as a portable, secure and concurrent programming language, the mostly concurrent garbage collector turned out to be an excellent solution for Java's garbage collection task. The use of this collector is reported for several modern production Java Virtual Machines and it has been investigated further in academia.In this paper, we present a modification of the mostly concurrent collector, which improves the throughput, the memory footprint, and the cache behavior of the collector without foiling the other good qualities (such as short pauses and high scalability). We implemented our solution on the IBM production JVM and obtained a performance improvement of up to 26.7%, a reduction in the heap consumption by up to 13.4%, and no substantial change in the (short) pause times. The modified algorithm was subsequently incorporated into the IBM production JVM.

The deployment of Java as a concurrent programming language has created a critical need for high-performance, concurrent, and incremental multiprocessor garbage collection. We present the Recycler , a fully concurrent pure reference counting garbage collector that we have implemented in the Jalapeño Java virtual machine running on shared memory multiprocessors. While a variety of multiprocessor collectors have been proposed and some have been implemented, experimental data is limited and there is little quantitative basis for comparison between different algorithms. We present measurements of the Recycler and compare it against a non-concurrent but parallel load-balancing mark-and-sweep collector (that we also implemented in Jalapeño), and evaluate the classical tradeoff between response time and throughput. When processor or memory resources are limited, the Recycler runs at about 90% of the speed of the mark-and-sweep collector. However, with an extra processor to run collection and with a moderate amount of memory headroom, the Recycler is able to operate without ever blocking the mutators and achieves a maximum measured mutator delay of only 2.6 milliseconds for our benchmarks. End-to-end execution time is usually within 5%.

The paper presents a generalization of Haskell's IO monad suitable for synchronous concurrent programming. The new monad integrates the deterministic concurrency paradigm of synchronous programming with the powerful abstraction features of functional languages and with full support for imperative programming. For event-driven applications, it offers an alternative to the use of existing, thread-based concurrency extensions of functional languages. The concepts presented have been applied in practice in a framework for programming interactive graphics.

This paper describes the development of the programming language Erlang during the period 1985--1997.Erlang is a concurrent programming language designed for programming large-scale distributed soft real-time control applications.The design of Erlang was heavily influenced by ideas from the logic and functional programming communities. Other sources of inspiration came from languages such as Chill and Ada which are used in industry for programming control systems.

Embedded systems are hard to program. Much of the effort is concentrated on processor-management code, effort totally unrelated to the application being built. Concurrent programming in embedded systems introduces even more problems --- mechanisms are needed to protect critical data areas. The application of object modeling to such mechanisms results in numerous benefits: fewer programming errors, enhanced portability and improved reuse. We present some simple in techniques for realising these benefits.

The term Inheritance Anomaly has been introduced into Object-Oriented Concurrent Programming (OOCP). It has also been shown how different kinds of synchronization mechanisms fall into one of the three anomalies. Guarded Methods are shown to be an inadequate tool to solve either History-only Sensitive Anomaly or Modification of Acceptable States. This paper argues that any of the anomalies can be solved by Guarded Methods when a suitable semantics is found for it. The main contribution of the paper is the exposition that the concept of Guarded Methods, provided Guarded Methods are interpreted as Conditional Critical Regions, is an adequate language tool for expressing synchronization constraints in OOCP. Guarded Method based solutions are given for the above mentioned two cases of anomalies.

In this paper, ALBA, A parallel Language Based on Actors, is introduced. ALBA [15] is a new programming language designed to take advantage of highly parallel architectures that use message passing as the fundamental low-level interaction primitive. ALBA is being developed as implementation language for the QUATRO parallel Database machine [5] in order to facilitate its portability and permit a homogeneous description of the QUATRO system to every multiprocessor machine.ALBA is a strong-typed language, and is oriented towards the development of both parallel and distributed applications. The actor paradigm in ALBA presents new characteristics such as the use of broadcast methods; dynamic actor allocations permitting the programmer to distribute actors on the machine, in a load-balancing way, on both a specific set of virtual processors or on all of the processors of the machine; different communication and synchronization mechanisms among actors, and others that are presented in this papcr.The ALBA programming language and the QUATRO Database Machine are being developed under the HELIOS operating system for a transputer machine.

ENSEMBLE is a programmming system for writing concurrent programs on a personal computer (PC).ENSEMBLE consists of a library of Turbo Pascal 1 units to be used with applications written in the same language and executable on IBM PCs or compatibles under the MS-DOS 2 operating system. ENSEMBLE provides the programmer with a set of facilities and predefined abstractions that simplify the construction of concurrent programs. The main abstractions are coroutines and tasks.ENSEMBLE's main goal is to provide an environment that can be easily used by students for gaining experience in a wide variety of concurrent programming models and techniques. However, ENSEMBLE was designed to be also a satisfactory production tool for writing concurrent and real-time software on a PC.

A typical problem of concurrent programming is to ensure the correct termination of the concurrent processes which implement a program. The concurrent language Occam 2 does not provide explicit mechanisms to handle the program termination. This paper describes how to implement the distributed termination of Occam programs expressed as a network of parallel processes, avoiding deadlock situations or never-ending execution. The technique is based on the propagation of a termination message down the network of processes. Some Occam 2 programs which use this technique are described.

Smalltalk-80 provides only a minimal set of concurrency control mechanisms. The fork and newProcess messages can be used to indicate that two (or more) processes can run concurrently, and a Semaphore class is provided which can be used to achieve synchronization.These features are not enough, however, to simulate true concurrency. A process will not yield the processor until it can no longer continue. This makes it all too easy to unintentionally produce code which is dependent upon yielding the processor at some specific point.The Delay and Random classes were used to force processes to yield nondeterministically. This allowed a single processor, context switching environment to be simulated. The producer/consumer problem was used to exercise the concurrent mechanisms in this investigation.

The integration of logic programming and concurrent programming has created a new class of languages, concurrent logic languages. These languages are born from a new interpretation of Horn clauses, called the process interpretation. The main goal of concurrent logic languages is the exploitation of parallelism which is inside logic programs. Furthermore, they extend the application areas of logic programming. This paper surveys and compares the two most significant concurrent programming languages, PARLOG and Concurrent Prolog. For both languages the main features are presented and discussed.

The talk extends the Laws of Programming [1] by four laws governing concurrent composition of programs. This operator is associative and commutative and distributive through union; and it has the same unit (do nothing) as sequential composition. Furthermore, sequential and concurrent composition distribute through each other, in accordance with an exchange law; this permits an implementation of concurrency by partial interleaving.

The aim of ÆMINIUM is to study the implications of having a concurrent-by-default programming language. This includes language design, runtime system, performance and software engineering considerations. We conduct our study through the design of the concurrent-by-default ÆMINIUM programming language. ÆMINIUM leverages the permission flow of object and group permissions through the program to validate the program's correctness and to automatically infer a possible parallelization strategy via a dataflow graph. ÆMINIUM supports not only fork-join parallelism but more general dataflow patterns of parallelism. In this paper we present a formal system, called μÆMINIUM, modeling the core concepts of ÆMINIUM. μÆMINIUM's static type system is based on Featherweight Java with ÆMINIUM-specific extensions. Besides checking for correctness ÆMINIUM's type system it also uses the permission flow to compute a potential parallel execution strategy for the program. μÆMINIUM's dynamic semantics use a concurrent-by-default evaluation approach. Along with the formal system we present its soundness proof. We provide a full description of the implementation along with the description of various optimization techniques we used. We implemented ÆMINIUM as an extension of the Plaid programming language, which has first-class support for permissions built-in. The ÆMINIUM implementation and all case studies are publicly available under the General Public License. We use various case studies to evaluate ÆMINIUM's applicability and to demonstrate that ÆMINIUM parallelized code has performance improvements compared to its sequential counterpart. We chose to use case studies from common domains or problems that are known to benefit from parallelization, to show that ÆMINIUM is powerful enough to encode them. We demonstrate through a webserver application, which evaluates ÆMINIUM's impact on latency-bound applications, that ÆMINIUM can achieve a 70% performance improvement over the sequential counterpart. In another case study we chose to implement a dictionary function to evaluate ÆMINIUM's capabilities to express essential data structures. Our evaluation demonstrates that ÆMINIUM can be used to express parallelism in such data-structures and that the performance benefits scale with the amount of annotation effort which is put into the implementation. We chose an integral computationally example to evaluate pure functional programming and computational intensive use cases. Our experiments show that ÆMINIUM is capable of extracting parallelism from functional code and achieving performance improvements up to the limits of Plaid's inherent performance bounds. Overall, we hope that the work helps to advance concurrent programming in modern programming environments.

Haskell has a rich set of synchronization primitives for implementing shared-state concurrency abstractions, ranging from the very high level (Software Transactional Memory) to the very low level (mutable variables with atomic read-modifywrite). In this paper we perform a systematic comparison of these different concurrent programming models by using them to implement the same abstraction: a concurrent linked-list. Our results are somewhat surprising: there is a full two orders of magnitude difference in performance between the slowest and the fastest implementation. Our analysis of the performance results gives new insights into the relative performance of the programming models and their implementation. Finally, we suggest the addition of a single primitive which in our experiments improves the performance of one of the STM-based implementations by more than a factor of 7.

The efficiency of Ada's rendezvous concept is compared with Concurrent Pascal's monitor concept. The differences between the two approaches, as well as a number of issues relating to their implementation, are presented. The results indicate that a concurrent programming language should provide both types of concepts.

LISPTALK is a concurrent language which is based on both LISP and CSP. It is a process-oriented language. Besides the idea of pure LISP and CSP, its main features are COTALK, CHANNEL-PORT, and LINK. Within a process there may exist many LISP functions which can be defined by recursion. The communication among processes uses INPUT and OUTPUT function through CHANNEL-PORT. The LINK connects the CHANNEL-PORTS of processes staticlly and synchronizes the communication. LISPTALK can be used to object-oriented programming like SMALLTALK-80. The language is also suit for vision understanding and robotics. The most interesting is the similarity between LISPTALK's structure and human brain structure.

This paper reports additions to Pascal-FC, a language designed to provide students of concurrent programming with practical experience of a variety of interprocess communication primitives. An earlier report in this journal described the facilities for using semaphores, monitors and an occam/CSP-style rendezvous. To these facilities have now been added an Ada-style rendezvous. An improved post-mortem dump has also been included.

This paper discusses some of the major design decisions that distiguish recent language proposals for concurrent programming, It is argued that the classification of languages as "procedure-based" or "message-based" is misleading, in that it confuses two independent issues. It is further argued that these issues are best left undecided by the language designer.

Pascal-FC is an extension of one of Wirth's simple Pascals. The added features allow processes to be specified and executed concurrently. Moreover communication and synchronisation primitives have been added to support semaphores, monitors and the CSP/occam type rendezvous. The language is used to give computer science students practical experience of a range of concurrency models.

ConcurrentSmalltalk is an object-oriented concurrent programming language/system which has been running since late 1985. ConcurrentSmalltalk has the following features: Upper-compatibility with Smalltalk-80. Asynchronous method calls and CBox objects yield concurrency. Atomic objects have the property of running one at a time so that it can serialize the many requests sent to it. Through experience in writing programs, some disadvantages have become apparent related to concurrency control and the behavior of a block context. In this paper, these issues are re-examined in detail, and then the evolution of the solutions for overcoming these shortcomings is described along with the model of computation in ConcurrentSmalltalk. New features are explained with an example program. The implementation of the ConcurrentSmalltalk virtual machine is also presented along with the evaluation of it.

In this paper primitives for asynchronous process communication are defined and added to the programming language Occam. Most of the existing concurrent programming concepts have synchronization mechanisms built-in the communication primitives degrading process independency and restricting the parallelism they are trying to provide. Asynchronous process communication provides more freedom in programming concurrent systems allowing non-blocking semantics for both send and receive primitives. Messages are buffered and a number of operations over buffered but not yet received messages are defined, allowing programmer to set or dynamically change the communication discipline needed for the particular application. The goal of the work presented is to relax strict process communication discipline and to make Occam more convenient for expressing concurrency needed for real-time applications. Although Occam is based on the synchronous communication model, its low level facilities provide a possibility to create the semantics of concurrency completely different from the one initially offered.

ConcurrentSmalltalk is a programming language/system which incorporates the facilities of concurrent programming in Smalltalk-80 1 . Such facilities are realized by providing concurrent constructs and atomic objects . This paper first gives an outline of ConcurrentSmalltalk. Then, the design of ConcurrentSmalltalk is described. The implementation of ConcurrentSmalltalk is presented in detail.

We present three new implementations of semaphores for V7 UNIX. None require kernel modifications. The canonical UNIX semaphore method uses link O in a spin loop. The first new method replaces the canonical spin loop with a software trap mechanism, the second provides additional enhancements in the form of a pool of semaphores and explicit quene management, and the third is a distributed protocol extending to the ability for synchronizing in network environments.

Presents a survey of some of the currently used languages. Design features of each are compared, and the applicability of each language to various programming tasks is examined. 27 references.