Programs written in concurrent object-oriented languages, especially ones that employ thread-safe reusable class libraries, can execute synchronization operations (lock, notify, etc.) at an amazing rate. Unless implemented with utmost care, synchronization can become a performance bottleneck. Furthermore, in languages where every object may have its own monitor, per-object space overhead must be minimized. To address these concerns, we have developed a meta-lock to mediate access to synchronization data. The meta-lock is fast (lock + unlock executes in 11 SPARC™ architecture instructions), compact (uses only two bits of space), robust under contention (no busy-waiting), and flexible (supports a variety of higher-level synchronization operations). We have validated the meta-lock with an implementation of the synchronization operations in a high-performance product-quality Java™ virtual machine and report performance data for several large programs.

Concurrent real-time systems are among the most difficult systems to design because of the many possible interleavings of events and because of the timing requirements that must be satisfied. We have developed a graphical environment based on Real-Time Graphical Interval Logic (RTGIL) for specifying and reasoning about the designs of concurrent real-time systems. Specifications in the logic have an intuitive graphical representation that resembles the timing diagrams drawn by software and hardware engineers, with real-time constraints that bound the durations of intervals. The syntax-directed editor of the RTGIL environment enables the user to compose and edit graphical formulas on a workstation display; the automated theorem prover mechanically checks the validity of proofs in the logic; and the database and proof manager tracks proof dependencies and allows formulas to be stored and retrieved. This article describes the logic, methodology, and tools that comprise the prototype RTGIL environment and illustrates the use of the environment with an example application.

This paper describes a generic tableau algorithm, which is the basis for a general customizable method for producing oracles from temporal logic specifications. A generic argument gives semantic rules with which to build the semantic tableau for a specification. Parameterizing the tableau algorithm by semantic rules permits it to easily accommodate a variety of temporal operators and provides a clean mechanism for fine-tuning the algorithm to produce efficient oracles.The paper develops conditions to ensure that a set of rules results in a correct tableau procedure. It gives sample rules for a variety of linear-time temporal operators and shows how rules are tailored to reduce the size of an oracle.

Interval logic has been introduced as a temporal logic that provides higher-level constructs and an intuitive graphical representation, making it easier in interval logic than in other temporal logics to specify and reason about concurrency in software and hardware designs. In this paper we present axiomatizations for two propositional interval logics and relate these logics to Until Temporal Logic. All of these logics are discrete linear-time temporal logics with no next operator. The next operator obstructs the use of hierarchical abstraction and refinement, and makes reasoning about concurrency difficult.

The Temporal Logic of Actions (TLA) devised by Lamport is a logic for proving the correctness of concurrent systems. A distinctive feature of the logic is the use of “action formulae” to encode the “before-after” behaviour of transitions, a feature that is especially suitable for Lamport's transition-axiom method. Abadi has given a complete axiomatization for the propositional fragment of this logic, and conjectured that its validity problem may be in PSPACE. In this paper we confirm that conjecture. In fact we show that the validity problem for TLA is PSPACE-complete. For this we give a space-optimal automata-theoretic decision procedure for TLA. Our result is obtained with respect to a logic which is a conservative extension of Lamport's TLA. Thus our decision procedure applies to the more restricted logic. We show how the automata-theoretic framework handles abstraction, as used in TLA, a feature considered useful for hierarchical and compositional reasoning.

We present axiomatizations for Until Temporal Logic (UTL) and for Since/Until Temporal Logic (SUTL). These logics are intended for use in specifying and reasoning about concurrent systems. They employ neither a next nor a previous operator, which obs

This article describes a graphical interval logic that is the foundation of a tool set supporting formal specification and verification of concurrent software systems. Experience has shown that most software engineers find standard temporal logics difficult to understand and use. The objective of this article is to enable software engineers to specify and reason about temporal properties of concurrent systems more easily by providing them with a logic that has an intuitive graphical representation and with tools that support its use. To illustrate the use of the graphical logic, the article provides some specifications for an elevator system and proves several properties of the specifications. The article also describes the tool set and the implementation.

Real-Time Future Interval Logic (RTFIL) is a visual logic with formulae that resemble timing diagrams. It is a dense real-time temporal logic that is based on two simple temporal primitives: interval modalities for the purely qualitative part and duration predicates for the quantitative part. We present the logic, and illustrate its use in specifying the railroad crossing example and in proving some of its properties. The logic is decidable by reduction to the emptiness problem of Timed Buchi Automata. An automated theorem prover based on this decision procedure has been implemented as part of a graphical proof environment. The proofs of the railroad crossing example have been verified using this theorem prover. An automated theorem prover and a graphical specification language greatly facilitate the task of verifying real-time proofs. This convenience apart, RTFIL is invariant under real-time stuttering and does not admit instantaneous states. These properties facilitate proof methods based on abstraction and refinement.>

We present a description of a graphical interval logic that is the foundation of a toolset we are developing to support formal specification and verification of concurrent software systems. Experience has shown that most software engineers find standard temporal logics difficult to under- stand and to use. Our objective is to enable software engineers to specify and reason about temporal properties of concurrent systems more easily by providing them with a logic that has an intuitive graphical representation and with tools that support its use. To illustrate the use of our graphical interval logic, we provide a specification for a readers/writers database system and prove several properties of the specification.