We present a computer-aided programming approach to concurrency. The approach allows programmers to program assuming a friendly, non-preemptive scheduler, and our synthesis procedure inserts synchronization to ensure that the final program works even with a preemptive scheduler. The correctness specification is implicit, inferred from the non-preemptive behavior. Let us consider sequences of calls that the program makes to an external interface. The specification requires that any such sequence produced under a preemptive scheduler should be included in the set of sequences produced under a non-preemptive scheduler. We guarantee that our synthesis does not introduce deadlocks and that the synchronization inserted is optimal w.r.t. a given objective function. The solution is based on a finitary abstraction, an algorithm for bounded language inclusion modulo an independence relation, and generation of a set of global constraints over synchronization placements. Each model of the global constraints set corresponds to a correctness-ensuring synchronization placement. The placement that is optimal w.r.t. the given objective function is chosen as the synchronization solution. We apply the approach to device-driver programming, where the driver threads call the software interface of the device and the API provided by the operating system. Our experiments demonstrate that our synthesis method is precise and efficient. The implicit specification helped us find one concurrency bug previously missed when model-checking using an explicit, user-provided specification. We implemented objective functions for coarse-grained and fine-grained locking and observed that different synchronization placements are produced for our experiments, favoring a minimal number of synchronization operations or maximum concurrency, respectively.

In this paper, we survey recent progress in CyberCardia project, a CPS Frontier project funded by the National Science Foundation. The CyberCardia project will lead to significant advances in the state of the art for system verification and cardiac therapies based on the use of formal methods and closed-loop control and verification. The animating vision for the work is to enable the development of a true in silico design methodology for medical devices that can be used to speed the development of new devices and to provide greater assurance that their behavior matches designer intentions, and to pass regulatory muster more quickly so that they can be used on patients needing their care. The acceleration in medical-device innovation achievable as a result of the CyberCardia research will also have long-term and sustained societal benefits, as better diagnostic and therapeutic technologies enter into the practice of medicine more quickly.

This paper presents general techniques for verifying virtually synchronous distributed control systems with interconnected physical environments. Such cyber-physical systems (CPSs) are notoriously hard to verify, due to their combination of nontrivial continuous dynamics, network delays, imprecise local clocks, asynchronous communication, etc. To simplify their analysis, we first extend the PALS methodology---that allows to abstract from the timing of events, asynchronous communication, network delays, and imprecise clocks, as long as the infrastructure guarantees bounds on the network delays and clock skews---from real-time to hybrid systems. We prove a bisimulation equivalence between Hybrid PALS synchronous and asynchronous models. We then show how various verification problems for synchronous Hybrid PALS models can be reduced to SMT solving over nonlinear theories of the real numbers. We illustrate the Hybrid PALS modeling and verification methodology on a number of CPSs, including a control system for turning an airplane.

In this work, we developed a methodology to analyze a bacteria model that mimics the stages through which bacteria change when phage therapy is applied. Due to the widespread misuse and overuse of antibiotics, drug resistant bacteria now pose significant risks to health, agriculture and the environment. Therefore, we were interested in an alternative to conventional antibiotics, a phage therapy. Our model was designed according to an experimental procedure to engineer a temperate phage, Lambda (λ), and then kill bacteria via light-activated production of superoxide. We applied formal analysis to our model and the results show that such an approach can speed up evaluation of the system, which would be impractical or possibly not even feasible to study in a wet lab.

Recent clinical studies suggest that the efficacy of hormone therapy for prostate cancer depends on the characteristics of individual patients. In this paper, we develop a computational framework for identifying patient-specific androgen ablation therapy schedules for postponing the potential cancer relapse. We model the population dynamics of heterogeneous prostate cancer cells in response to androgen suppression as a nonlinear hybrid automaton. We estimate personalized kinetic parameters to characterize patients and employ δ-reachability analysis to predict patient-specific therapeutic strategies. The results show that our methods are promising and may lead to a prognostic tool for prostate cancer therapy.

In this paper we address the problem of verifying in stochastic hybrid systems temporal logic properties whose probability of being true is very small --- rare events. It is well known that sampling-based (Monte Carlo) techniques, such as statistical model checking, do not perform well for estimating rare-event probabilities. The problem is that the sample size required for good accuracy grows too large as the event probability tends to zero. However, several techniques have been developed to address this problem. We focus on importance sampling techniques, which bias the original system to compute highly accurate and efficient estimates. The main difficulty in importance sampling is to devise a good biasing density, that is, a density yielding a low-variance estimator. In this paper, we show how to use the cross-entropy method for generating approximately optimal biasing densities for statistical model checking. We apply the method with importance sampling and statistical model checking for estimating rare-event probabilities in stochastic hybrid systems coded as Stateflow/Simulink diagrams.

Given any collection F of computable functions over the reals, we show that there exists an algorithm that, given any sentence A containing only bounded quantifiers and functions in F, and any positive rational number delta, decides either “A is true”, or “a delta-strengthening of A is false”. Moreover, if F can be computed in complexity class C, then under mild assumptions, this “delta-decision problem” for bounded Sigma k-sentences resides in Sigma k(C). The results stand in sharp contrast to the well-known undecidability of the general first-order theories with these functions, and serve as a theoretical basis for the use of numerical methods in decision procedures for formulas over the reals.

We consider the problem of learning a non-deterministic probabilistic system consistent with a given finite set of positive and negative tree samples. Consistency is defined with respect to strong simulation conformance. We propose learning algorithms that use traditional and a new stochastic state-space partitioning, the latter resulting in the minimum number of states. We then use them to solve the problem of active learning, that uses a knowledgeable teacher to generate samples as counterexamples to simulation equivalence queries. We show that the problem is undecidable in general, but that it becomes decidable under a suitable condition on the teacher which comes naturally from the way samples are generated from failed simulation checks. The latter problem is shown to be undecidable if we impose an additional condition on the learner to always conjecture a minimum state hypothesis. We therefore propose a semi-algorithm using stochastic partitions. Finally, we apply the proposed (semi-) algorithms to infer intermediate assumptions in an automated assume-guarantee verification framework for probabilistic systems.

We show how statistical Model Checking can be used for verifying properties of analog circuits. As integrated circuit technologies scale down, manufacturing variations in devices make analog designs behave like stochastic systems. The problem of verifying stochastic systems is often difficult because of their large state space. Statistical Model Checking can be an efficient verification technique for stochastic systems. In this paper, we use sequential statistical techniques and model checking to verify properties of analog circuits in both the temporal and the frequency domain. In particular, randomly sampled system traces are sequentially generated by SPICE and passed to a trace checker to determine whether they satisfy a given specification, until the desired statistical strength is achieved.

We address the problem of model checking stochastic systems, i.e.~checking whether a stochastic system satisfies a certain temporal property with a probability greater (or smaller) than a fixed threshold. In particular, we present a novel Statistical Model Checking (SMC) approach based on Bayesian statistics. We show that our approach is feasible for hybrid systems with stochastic transitions, a generalization of Simulink/Stateflow models. Standard approaches to stochastic (discrete) systems require numerical solutions for large optimization problems and quickly become infeasible with larger state spaces. Generalizations of these techniques to hybrid systems with stochastic effects are even more challenging. The SMC approach was pioneered by Younes and Simmons in the discrete and non-Bayesian case. It solves the verification problem by combining randomized sampling of system traces (which is very efficient for Simulink/Stateflow) with hypothesis testing or estimation. We believe SMC is essential for scaling up to large Stateflow/Simulink models. While the answer to the verification problem is not guaranteed to be correct, we prove that Bayesian SMC can make the probability of giving a wrong answer arbitrarily small. The advantage is that answers can usually be obtained much faster than with standard, exhaustive model checking techniques. We apply our Bayesian SMC approach to a representative example of stochastic discrete-time hybrid system models in Stateflow/Simulink: a fuel control system featuring hybrid behavior and fault tolerance. We show that our technique enables faster verification than state-of-the-art statistical techniques, while retaining the same error bounds. We emphasize that Bayesian SMC is by no means restricted to Stateflow/Simulink models: we have in fact successfully applied it to very large stochastic models from Systems Biology.

BACKGROUND: Recent studies have found that overexpression of the High-mobility group box-1 (HMGB1) protein, in conjunction with its receptors for advanced glycation end products (RAGEs) and toll-like receptors (TLRs), is associated with proliferation of various cancer types, including that of the breast and pancreatic. RESULTS: We have developed a rule-based model of crosstalk between the HMGB1 signaling pathway and other key cancer signaling pathways. The model has been simulated using both ordinary differential equations (ODEs) and discrete stochastic simulation. We have applied an automated verification technique, Statistical Model Checking, to validate interesting temporal properties of our model. CONCLUSIONS: Our simulations show that, if HMGB1 is overexpressed, then the oncoproteins CyclinD/E, which regulate cell proliferation, are overexpressed, while tumor suppressor proteins that regulate cell apoptosis (programmed cell death), such as p53, are repressed. Discrete, stochastic simulations show that p53 and MDM2 oscillations continue even after 10 hours, as observed by experiments. This property is not exhibited by the deterministic ODE simulation, for the chosen parameters. Moreover, the models also predict that mutations of RAS, ARF and P21 in the context of HMGB1 signaling can influence the cancer cell's fate - apoptosis or survival - through the crosstalk of different pathways.

Boolean satisfiability (SAT) solvers are used heavily in hardware and software verification tools for checking satisfiability of Boolean formulas. Most state-of-the-art SAT solvers are based on the Davis-Putnam-Logemann-Loveland (DPLL) algorithm and require the input formula to be in conjunctive normal form (CNF). We present a new SAT solver that operates on the negation normal form (NNF) of the given Boolean formulas/circuits. The NNF of a formula is usually more succinct than the CNF of the formula in terms of the number of variables. Our algorithm applies the DPLL algorithm to the graph-based representations of NNF formulas. We adapt the idea of the two-watched-literal scheme from CNF SAT solvers in order to efficiently carry out Boolean Constraint Propagation (BCP), a key task in the DPLL algorithm. We evaluate the new solver on a large collection of Boolean circuit benchmarks obtained from formal verification problems. The new solver outperforms the top solvers of the SAT 2007 competition and SAT-Race 2008 in terms of run time on a large majority of the benchmarks.

Model checking is an automatic verification technique for state-transition systems that are finite-state or that have finite-state abstractions. In the early 1980's in a series of joint papers with my graduate students E.A. Emerson and A.P. Sistla, we proposed that model checking could be used for verifying concurrent systems and gave algorithms for this purpose. At roughly the same time, Joseph Sifakis and his student J.P. Queille at the University of Grenoble independently developed a similar technique. Model checking has been used successfully to reason about computer hardware and communication protocols and is beginning to be used for verifying computer software. Specifications are written in temporal logic, which is particularly valuable for expressing concurrency properties. An intelligent, exhaustive search is used to determine if the specification is true or not. If the specification is not true, the model checker will produce a counterexample execution trace that shows why the specification does not hold. This feature is extremely useful for finding obscure errors in complex systems. The main disadvantage of model checking is the state-explosion problem, which can occur if the system under verification has many processes or complex data structures. Although the state-explosion problem is inevitable in worst case, over the past 27 years considerable progress has been made on the problem for certain classes of state-transition systems that occur often in practice. In this talk, I will describe what model checking is, how it works, and the main techniques that have been developed for combating the state explosion problem.

As a first step, most model checkers used in the hardware industry convert a high-level register-transfer-level (RTL) design into a netlist. However, algorithms that operate at the netlist level are unable to exploit the structure of the higher abstraction levels and, thus, are less scalable. The RTL of a hardware description language such as Verilog is similar to a software program with special features for hardware design such as bit-vector arithmetic and concurrency. This paper uses predicate abstraction, a software verification technique, for verifying RTL Verilog. There are two challenges when applying predicate abstraction to circuits: 1) the computation of the abstract model in presence of a large number of predicates and 2) the discovery of suitable word-level predicates for abstraction refinement. We address the first problem using a technique called predicate clustering. We address the second problem by computing the weakest preconditions of Verilog statements in order to obtain new word-level predicates during abstraction refinement. We compare the performance of our technique with localization reduction, a netlist-level abstraction technique, and report improvements on a set of benchmarks.

Model checking techniques applied to large industrial circuits suffer from the state space explosion problem. A major technique to address this problem is abstraction. The most commonly used abstraction technique for hardware verification is localization reduction, which removes latches that are not relevant to the property. However, localization reduction fails to reduce the size of the model if the property actually depends on most of the latches. This paper proposes to use predicate abstraction for verifying RTL Verilog, a technique successfully used for software verification. The main challenge when using predicate abstraction is the discovery of suitable predicates. We propose to use weakest preconditions of Verilog statements in order to obtain new predicates during abstraction refinement. This technique has not been applied to circuits before. On benchmarks taken from an industrial microprocessor, we successfully verified safety properties with more than 32,000 latches in the cone of influence. We compare the performance of our technique with a modern model checker that implements localization reduction.

Abstraction techniques have been very successful in model checking large systems by enabling the model checker to ignore irrelevant details. Most abstraction techniques in literature are based on refinement. We introduce the notion of broken traces which capture the necessary and sufficient conditions for the existence of an error path in the abstract model. We formulate abstraction as learning the abstract model from samples of broken traces. Our iterative algorithm for abstraction-based model checking is not based on refinement and can generate the smallest abstract model that proves the property. We present an implementation of this algorithm for the verification of safety properties on gate-level net-lists with localization abstraction. Experimental results prove the viability of our techniques.

Abstract We present a framework for model checking concurrent software systems which incorporates both states and events. Contrary to other state/event approaches, our work also integrates two powerful verification techniques, counterexample-guided abstraction refinement and compositional reasoning. Our specification language is a state/event extension of linear temporal logic, and allows us to express many properties of software in a concise and intuitive manner. We show how standard automata-theoretic LTL model checking algorithms can be ported to our framework at no extra cost, enabling us to directly benefit from the large body of research on efficient LTL verification. We also present an algorithm to detect deadlocks in concurrent message-passing programs. Deadlock- freedom is not only an important and desirable property in its own right, but is also a prerequisite for the soundness of our model checking algorithm. Even though deadlock is inherently non-compositional and is not preserved by classical abstractions, our iterative algorithm employs both (non-standard) abstractions and compositional reasoning to alleviate the state-space explosion problem. The resulting framework differs in key respects from other instances of the counterexample-guided abstraction refinement paradigm found in the literature. We have implemented this work in the magic verification tool for concurrent C programs and performed tests on a broad set of benchmarks. Our experiments show that this new approach not only eases the writing of specifications, but also yields important gains both in space and in time during verification. In certain cases, we even encountered specifications that could not be verified using traditional pure event-based or state-based approaches, but became tractable within our state/event framework. We also recorded substantial reductions in time and memory consumption when performing deadlock-freedom checks with our new abstractions. Finally, we report two bugs (including a deadlock) in the source code of Micro-C/OS versions 2.0 and 2.7, which we discovered during our experiments.

MAGIC is a software verification project for C source code which verifies conformance of software components against statemachine specifications. To this aim, MAGIC extracts abstract software models using predicate abstraction, and resolves the inherent trade-off between model accuracy and scalability by an iterative abstraction refinement methodology. This paper presents the core principles implemented in the MAGIC verification engine, i.e. specification conformance using simulation and abstraction refinement. Viewing counterexamples as winning strategies in a simulation game between the implementation and the specification, we describe an algorithm where abstractions are refined on the basis of multiple winning strategies simultaneously. The refinement process is iterated until either a conformance with the specification is established, or a strategy to violate the specification is found to be realizable. In addition to the increase in expressiveness achieved by using simulation instead of trace containment, experimental results using OpenSSL indicate that our approach can lead to orders of magnitude improvement in verification time.

Parametric representations used for symbolic simulation of circuits usually use BDDs. After a few steps of symbolic simulation, state set representation is converted from one parametric representation to another smaller representation, in a process called reparameterization. For large circuits, the reparametrization step often results in a blowup of BDDs and is expensive due to a large number of quantifications of input variables involved. Efficient SAT solvers have been applied successfully for many verification problems. This paper presents a novel SAT-based reparameterization algorithm that is largely immune to the large number of input variables that need to be quantified. We show experimental results on large industrial circuits and compare our new algorithm to both SAT-based Bounded Model Checking and BDD based symbolic simulation. We were able to achieve on average 3x improvement in time and space over BMC and able to complete many examples that BDD based approach could not even finish.

It is common practice to write C models of circuits due to the greater simulation efficiency. Once the C program satisfies the requirements, the circuit is designed in a hardware description language (HDL) such as Verilog. It is therefore highly desirable to automatically perform a correspondence check between the C model and a circuit given in HDL. We present an algorithm that checks consistency between an ANSI-C program and a circuit given in Verilog using predicate abstraction. The algorithm exploits the fact that the C program and the circuit share many basic predicates. In contrast to existing tools that perform predicate abstraction, our approach is SAT-based and allows all ANSI-C and Verilog operators in the predicates. We report experimental results on an out-of-order RISC processor. We compare the performance of the new technique to bounded model checking (BMC).

We present an algorithm to detect deadlocks in concurrent message-passing programs. Even though deadlock is inherently noncompositional and its absence is not preserved by standard abstractions, our framework employs both abstraction and compositional reasoning to alleviate the state space explosion problem. We iteratively construct increasingly more precise abstractions on the basis of spurious counterexamples to either detect a deadlock or prove that no deadlock exists. Our approach is inspired by the counterexample-guided abstraction refinement paradigm. However, our notion of abstraction as well as our schemes for verification and abstraction refinement differs in key respects from existing abstraction refinement frameworks. Our algorithm is also compositional in that abstraction, counterexample validation, and refinement are all carried out component-wise and do not require the construction of the complete state space of the concrete system under consideration. Finally, our approach is completely automated and provides diagnostic feedback in case a deadlock is detected. We have implemented our technique in the MAGIC verification tool and present encouraging results (up to 20 times speed-up in time and 4 times less memory consumption) with concurrent message-passing C programs. We also report a bug in the real-time operating system MicroC/OS version 2.70.

Languages such as SystemC or SpecC offer a new design paradigm that addresses the industry's need for a fast time-to-market. However, formal verification techniques are widely applied in the hardware design industry only for low level designs, such as a netlist or RTL. The higher abstraction levels offered by these new languages are not yet amenable to rigorous, formal verification. This paper describes how to apply predicate abstraction to SpecC system descriptions. The technique supports the concurrency constructs offered by SpecC. It models the bit-vector semantics of the language accurately, and can be used for both property checking and for checking refinement together with a traditional low-level design given in Verilog.

We describe new techniques for model checking in the counterexample-guided abstraction-refinement framework. The abstraction phase "hides" the logic of various variables, hence considering them as inputs. This type of abstraction may lead to "spurious" counterexamples, i.e., traces that cannot be simulated on the original (concrete) machine. We check whether a counterexample is real or spurious with a satisfiability (SAT) checker. We then use a combination of 0-1 integer linear programming and machine learning techniques for refining the abstraction based on the counterexample. The process is repeated until either a real counterexample is found or the property is verified. We have implemented these techniques on top of the model checker NuSMV and the SAT solver Chaff. Experimental results prove the viability of these new techniques.

We present a new methodology for automatic verification of C programs against finite state machine specifications. Our approach is compositional, naturally enabling us to decompose the verification of large software systems into subproblems of manageable complexity. The decomposition reflects the modularity in the software design. We use weak simulation as the notion of conformance between the program and its specification. Following the counterexample guided abstraction refinement (CEGAR) paradigm, our tool MAGIC first extracts a finite model from C source code using predicate abstraction and theorem proving. Subsequently, weak simulation is checked via a reduction to Boolean satisfiability. MAGIC has been interfaced with several publicly available theorem provers and SAT solvers. We report experimental results with procedures from the Linux kernel, the OpenSSL toolkit, and several industrial strength benchmarks.

We describe an algorithm to verify a hardware design given in Verilog using an ANSI-C program as a specification. We use SAT based Bounded Model Checking [1] in order to reduce the equivalence problem to a bit vector logic decision problem. As a case study, we describe experimental results on a hardware and a software implementation of the data encryption standard (DES) algorithm.

Abstract: "We present an algorithm that checks behavioral consistency between an ANSI-C program and a circuit given in Verilog using Bounded Model Checking. Both the circuit and the program are unwound and translated into a formula that is satisfiable if and only if the circuit and the code disagree. The formula is then checked using a SAT solver. We are able to translate C programs that make use of side effects, pointers, dynamic memory allocation, and loops with conditions that cannot be evaluated statically. We describe experimental results on various reactive circuits and programs, including a small processor given in Verilog and its Instruction Set Architecture given in ANSI-C."

Multiple clock domains are a challenge for hardware specification and verification. We present a method for specifying the relations between multiple clocks, and for modeling the possible behaviors. We can then verify a hardware design assuming that the clocks meet these constraints. We implement our ideas in the context of SAT based bounded model checking (BMC), using ANSI-C programs to specify the functional behavior of the design.

We introduce a new method for two-level logic minimization. Unlike previous approaches, the new method uses a SAT solver as an underlying engine. While the overall minimization strategy of the new method is based on the operators as defined in ESPRESSO-II, our SAT-based implementation is significantly different. The new minimizer SAT-ESPRESSO was found to perform 5-20 times faster than ESPRESSO-II and 3-5 times faster than BOOM on a set of large examples.

We present a new methodology for automatic verification of C programs against finite state machine specifications. Our approach is compositional, naturally enabling us to decompose the verification of large software systems into subproblems of manageable complexity. The decomposition reflects the modularity in the software design. We use weak simulation as the notion of conformance between the program and its specification. Following the abstract-verify-refine paradigm, our tool MAGIC first extracts a finite model from C source code using predicate abstraction and theorem proving. Subsequently, simulation is checked via a reduction to Boolean satisfiability. MAGIC is able to interface with several publicly available theorem provers and SAT solvers. We report experimental results with procedures from the Linux kernel and the OpenSSL toolkit.

Predicate abstraction has been widely used for model checking hardware/software systems. However, for control intensive systems, existing predicate abstraction techniques can potentially result in a blowup of the size of the abstract model. We deal with this problem by retaining important control variables in the abstract model. By this method we avoid having to introduce an unreasonable number of predicates to simulate the behavior of the control variables. We also show how to improve predicate abstraction by extracting useful information from a high level representation of hardware/software systems. This technique works by first extracting relevant branch conditions. These branch conditions are used to invalidate spurious abstract counterexamples through a new counterexample-based lazy refinement algorithm. Experimental results are included to demonstrate the effectiveness of our methods.

The main practical problem in model checking is the combinatorial explosion of system states commonly known as the state explosion problem. Abstraction methods attempt to reduce the size of the state space by employing knowledge about the system and the specification in order to model only relevant features in the Kripke structure. Counterexample-guided abstraction refinement is an automatic abstraction method where, starting with a relatively small skeletal representation of the system to be verified, increasingly precise abstract representations of the system are computed. The key step is to extract information from false negatives ("spurious counterexamples") due to over-approximation.

The state explosion problem remains a major hurdle in applying symbolic model checking to large hardware designs. State space abstraction, having been essential for verifying designs of industrial complexity, is typically a manual process, requiring considerable creativity and insight.In this article, we present an automatic iterative abstraction-refinement methodology that extends symbolic model checking. In our method, the initial abstract model is generated by an automatic analysis of the control structures in the program to be verified. Abstract models may admit erroneous (or "spurious") counterexamples. We devise new symbolic techniques that analyze such counterexamples and refine the abstract model correspondingly. We describe aSMV, a prototype implementation of our methodology in NuSMV. Practical experiments including a large Fujitsu IP core design with about 500 latches and 10000 lines of SMV code confirm the effectiveness of our approach.

We describe new techniques for model checking in the counterexample guided abstraction/refinement framework. The abstraction phase ‘hides’ the logic of various variables, hence considering them as inputs. This type of abstraction may lead to ‘spurious’ counterexamples, i.e. traces that can not be simulated on the original (concrete) machine. We check whether a counterexample is real or spurious with a SAT checker. We then use a combination of Integer Linear Programming (ILP) and machine learning techniques for refining the abstraction based on the counterexample. The process is repeated until either a real counterexample is found or the property is verified. We have implemented these techniques on top of the model checker NuSMV and the SAT solver Chaff. Experimental results prove the viability of these new techniques. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Counter examples for specification violations provide engineers with important debugging information. Although counterexamples are considered one of the main advantages of model checking, state-of the art model checkers are restricted to relatively simple counterexamples, and surprisingly little research effort has been put into counterexamples. In this paper, we introduce a new general framework for counterexamples. The paper has three main contributions: (i) We determine the general form of ACTL counterexamples. To this end, we investigate the notion of counterexample and show that a large class of temporal logics beyond ACTL admits counterexamples with a simple tree-like transition relation. We show that the existence of tree-like counterexamples is related to a universal fragment of extended branching time logic based on w-regular temporal operators. (ii) We present new symbolic algorithms to generate tree-like counterexamples for ACTL specifications. (iii) Based on tree-like counterexamples we extend the abstraction refinement methodology developed recently by Clarke et al. (CAV'2000) to full ACTL. This demonstrates the conceptual simplicity and elegance of tree-like counterexamples.

Computing the set of states reachable in one step from a given set of states, i.e. image computation, is a crucial step in several symbolic verification algorithms, including model checking and reachability analysis. So far, the best methods for quantification scheduling in image computation, with a conjunctively partitioned transition relation, have been restricted to a linear schedule. This results in a loss of flexibility during image computation. We view image computation as a problem of constructing an optimal parse tree for the image set. The optimality of a parse tree is defined by the largest BDD that is encountered during the computation of the tree. We present dynamic and static versions of a new algorithm, VarScore, which exploits the flexibility offered by the parse tree approach to the image computation. We show by extensive experimentation that our techniques outperform the best known techniques so far.

Implicit invocation or publish-subscribe has become an important architectural style for large-scale system design and evolution. The publish-subscribe style facilitates developing large-scale systems by composing separately developed components because the style permits loose coupling between various components. One of the major bottlenecks in using publish-subscribe systems for very large scale systems is the efficiency of filtering incoming messages, i.e., matching of published events with event subscriptions. This is a very challenging problem because in a realistic publish subscribe system the number of subscriptions can be large. We present an approach for matching published events with subscriptions which scales to a large number of subscriptions. Our approach uses binary decision diagrams, a compact data structure for representing Boolean functions which has been successfully used in verification techniques such as model checking. Experimental results clearly demonstrate the efficiency of our approach.

Variable ordering for BDDs has been extensively investigated. Recently, sampling based ordering techniques have been proposed to overcome problems with structure based static ordering methods and sifting based dynamic reordering techniques. However, existing sampling techniques can lead to an unacceptably large deviation in the size of the final BDD. In this paper, we propose a new sampling technique based on abstract BDDs (aBDDs) that does not suffer from this problem. This new technique, easy to implement and automate, consistently creates high quality variable orderings for both combinational as well as sequential functions. Experimental results show that for many applications our approach is significantly superior to existing techniques.

Due to the rapid growth of the “Internet” and the “World Wide Web” security has become a very important concern in the design and implementation of software systems. Since security has become an important issue, the number of protocols in this domain has become very large. These protocols are very diverse in nature. If a software architect wants to deploy some of these protocols in a system, they have to be sure that the protocol has the right properties as dictated by the requirements of the system. In this article we present BRUTUS, a tool for verifying properties of security protocols. This tool can be viewed as a special-purpose model checker for security protocols. We also present reduction techniques that make the tool efficient. Experimental results are provided to demonstrate the efficiency of BRUTUS.

Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of NSF or the United States Government. The U. S. Government is authorized to reproduce and distribute reprints for Government purposes notwithstanding any copyright notation thereon. This manuscript is submitted for publication with the understanding that the U. S. Government is authorized to reproduce and distribute reprints for Governmental purposes.

We introduce a new equivalence checking method based on abstract BDDs (aBDDs). The basic idea is the following: given an abstraction function, aBDDs reduce the size of BDDs by merging nodes that have the same abstract value. An aBDD has bounded size and can be constructed without constructing the original BDD. We show that this method of equivalence checking is always sound. It is complete for an important class of arithmetic circuits that includes integer multiplication. We also suggest heuristics for findings suitable abstraction functions based on the structure of the circuit. The efficiency of this technique is illustrated by experiments on ISCAS'85 benchmark circuits.

This article describes a technique based on network grammars and abstraction to verify families of state-transition systems. The family of state-transition systems is represented by a context-free network grammar. Using the structure of the network grammar our technique constructs a process invariant that simulates all the state-transition systems in the family. A novel idea introduced in this article is the use of regular languages to express state properties. We have implemented our techniques and verified two nontrivial examples.

Article Free Access Share on Word level model checking—avoiding the Pentium FDIV error Authors: E. M. Clarke School of Computer Science, Carnegie Mellon University, Pittsburgh, PA School of Computer Science, Carnegie Mellon University, Pittsburgh, PAView Profile , M. Khaira Intel Development Labs., Intel Corporation, 5200 NE Elam Young Pkwy, Hillsboro, OR Intel Development Labs., Intel Corporation, 5200 NE Elam Young Pkwy, Hillsboro, ORView Profile , X. Zhao School of Computer Science, Carnegie Mellon University, Pittsburgh, PA and Intel Development Labs., Intel Corporation, 5200 NE Elam Young Pkwy, Hillsboro, OR School of Computer Science, Carnegie Mellon University, Pittsburgh, PA and Intel Development Labs., Intel Corporation, 5200 NE Elam Young Pkwy, Hillsboro, ORView Profile Authors Info & Claims DAC '96: Proceedings of the 33rd annual Design Automation ConferenceJune 1996 Pages 645–648https://doi.org/10.1145/240518.240640Published:01 June 1996Publication History 20citation393DownloadsMetricsTotal Citations20Total Downloads393Last 12 Months52Last 6 weeks7 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

This paper illustrates the use of symbolic model checking in the design of deadlock-free flexible manufacturing systems. Our verification methodology consists of the following stages. First, we extract a state machine model of the system. Second, we write the system specifications using a propositional temporal logic. Finally we use the model checker to check the state machine of the system against its requirements. When a deadlock is identified, a counterexample is automatically generated with a scenario that leads to the deadlock. The counterexample is used to design the proper operational policy that will prevent the corresponding deadlock. This verification approach allows an exhaustive search of all possible behaviors and scenarios. We designed a flexible manufacturing system capable of producing 3 types of parts with 4 machines and 3 robots. It took 8 seconds to find possible deadlocks assuming machine processing capacity of one part at a time and about 36 seconds when we increased the machine processing capacity to two parts at a time. The size of the state space was in the order of 10/sup 18/ states.

Model checking is an automatic technique for verifying sequential circuit designs and protocols. An efficient search procedure is used to determine whether or not the specification is satisfied. If it is not satisfied, our technique will produce a counterexample execution trace that shows the cause of the problem. We describe an efficient algorithm to produce counterexamples and witnesses for symbolic model checking algorithms. This algorithm is used in the SMV model checker and works quite well in practice. We also discuss how to extend our technique to more complicated specifications.

Functions that map boolean vectors into the integers are important for the design and verification of arithmetic circuits. MTBDDs and BMDs have been proposed for representing this class of functions. We discuss the relationship between these methods and describe a generalization called hybrid decision diagrams which is often much more concise. We show how to implement arithmetic operations efficiently for hybrid decision diagrams. In practice, this is one of the main limitations of BMDs since performing arithmetic operations on functions expressed in this notation can be very expensive. In order to extend symbolic model checking algorithms to handle arithmetic properties, it is essential to be able to compute the BDD for the set of variable assignments that satisfy an arithmetic relation. In our paper, we give an efficient algorithm for this purpose. Moreover, we prove that for the class of linear expressions, the time complexity of our algorithm is linear in the number of variables.

Symbolic model checking is a successful technique for checking properties of large finite-state systems. This method has been used to verify a number of real-world hardware designs; however it is not able to determine timing or performance properties directly. Since these properties are extremely important in the design of high-performance systems and in time-critical applications, we have extended model checking techniques to produce timing information. Our results allow a more detailed analysis of a model than is possible with tools that simply determine whether a property is satisfied or not. We present algorithms that determine the exact bounds on the time interval between two specified events and the number of occurrences of another event in such an interval. To demonstrate how our method works, we have modelled the PCI local bus and analyzed its temporal behavior. The results demonstrate the usefulness of our technique in analyzing complex modem designs.

We show very efficient methods to compute Walsh spectrum for logic functions with large numbers of inputs (30 or more) using Binary Decision Diagrams. The BUD structure is extended to have any integer values as leaf (constant) nodes. The result is an efficient representation for integer vectors and integer matrices. The proposed procedure works directly on an extended BDD for the logic function, and computes the full Walsh spectrum in the form of an extended BDD. The algorithm presented is a more efficient version of the matrix-multiplication method. Our method embeds the Walsh transform matrix implicitly into program code with recursive calls, which results in a significant speed improvement. Our algorithm has the same complexity as the fastest known Walsh algorithm, and utilizes a much more efficient data structure than traditional truth tables. Furthermore, in cases where the complete set of spectra coefficient is either infeasible or impractical, we also present a method to compute subsets of Walsh coefficients. We present experimental results showing that logic functions having more than 60 inputs which cannot be processed by other published methods can be computed within 30 seconds on Sparc 2.>

Logical errors in finite-state concurrent systems such as sequential circuit designs and communication protocols are an important problem for computer scientists. A research group has developed a verification method called temporal logic model checking for this class of systems. In this approach specifications are expressed in a propositional temporal logic, while circuits and protocols are modeled as state-transition systems. An efficient search procedure is used to determine automatically if a specification is satisfied by some transition system. The technique has been used to find subtle errors in a number of non-trivial examples. During the last few years, the size of the state-transition systems that can be verified by model checking techniques has increased dramatically. By representing transition relations implicitly using binary decision diagrams (BDDs), we have been able to check some examples that would have required 10/sup 20/ states with the original algorithm. Various refinements of the BDD-based techniques have pushed the state count up to 10/sup 100/. By combining model checking with various abstraction techniques, we have been able to handle even larger systems. We focus on four of the most important directions for research: use of abstraction and symmetry to achieve an even greater reduction in the size of the state-space that must be explored by this method; development of model checking techniques that can handle parameterized designs without requiring each individual instance of the design to be verified; use of partial order semantics to avoid the state explosion problem that can occur in loosely coupled systems when concurrency is modeled by interleaving; determination of appropriate models and verification techniques for circuits and protocols with real-time constraints.>

Presents a general method for computing quantitative information about finite-state real-time systems. We have developed algorithms that compute exact bounds on the delay between two specified events and on the number of occurrences of an event in a given interval. This technique allows us to determine performance measures such as schedulability, response time, and system load. Our algorithms produce more detailed information than traditional methods. This information leads to a better understanding of system behavior, in addition to determining its correctness. The algorithms presented in this paper are efficiently implemented using binary decision diagrams and have been incorporated into the SMV symbolic model verifier. Using this method, we have verified a model of an aircraft control system with 10/sup 15/ states. The results obtained demonstrate that our method can be successfully applied in the verification of real-time system designs.>

The temporal logic model checking algorithm of Clarke, Emerson, and Sistla (1986) is modified to represent state graphs using binary decision diagrams (BDD's) and partitioned transition relations. Because this representation captures some of the regularity in the state space of circuits with data path logic, we are able to verify circuits with an extremely large number of states. We demonstrate this new technique on a synchronous pipelined design with approximately 5/spl times/10/sup 120/ states. Our model checking algorithm handles full CTL with fairness constraints. Consequently, we are able to express a number of important liveness and fairness properties, which would otherwise not be expressible in CTL. We give empirical results on the performance of the algorithm applied to both synchronous and asynchronous circuits with data path logic.>

We describe a method for using abstraction to reduce the complexity of temporal-logic model checking. Using techniques similar to those involved in abstract interpretation, we construct an abstract model of a program without ever examining the corresponding unabstracted model. We show how this abstract model can be used to verify properties of the original program. We have implemented a system based on these techniques, and we demonstrate their practicality using a number of examples, including a program representing a pipelined ALU circuit with over 10 1300 states.

The Walsh transform has numerous applications in computer-aided design, but the usefulness of these tech-niques in practice has been limited by the size of the boolean functions that can be transformed. Currently available techniques limit the functions to less than 20 variables. In this paper, we show how to compute concise representations of the Walsh transform for functions with several hundred vari-ables. We have applied our techniques to boolean technolqy mapping and, in certain cases, we obtained a speed up of as much as 50 % for the matching phase.

We describe a method for using abstraction to reduce the complexity of temporal logic model checking. The basis of this method is a way of constructing an abstract model of a program without ever examining the corresponding unabstracted model. We show how this abstract model can be used to verify properties of the original program. We have implemented a system based on these techniques, and we demonstrate their practicality using a number of examples, including a pipelined ALU circuit with over 101300 states.

The paper provides a synthesis between two main approaches to automatic verification of finite-state systems: temporal logic model checking and language containment of automata on infinite tapes. A new branching-time temporal logic is suggested, in which automata on infinite tapes are used to define new temporal operators. Each such operator defines a set of acceptable computation paths. Path quantifiers are used to specify whether all paths or some path from a state should be in some acceptable set. The logic is very powerful and includes both linear-time and branching-time temporal logics. We give an efficient model checking procedure that checks whether a finite-state system satisfies its specification, given by a formula of the new logic. Our procedure is linear in the size of the system and a low level polynomial in the size of the specification.

Article Representing circuits more efficiently in symbolic model checking Share on Authors: J. R. Burch School of Computer Science, Carnegie Mellon University School of Computer Science, Carnegie Mellon UniversityView Profile , E. M. Clarke School of Computer Science, Carnegie Mellon University School of Computer Science, Carnegie Mellon UniversityView Profile , D. E. Long School of Computer Science, Carnegie Mellon University School of Computer Science, Carnegie Mellon UniversityView Profile Authors Info & Claims DAC '91: Proceedings of the 28th ACM/IEEE Design Automation ConferenceJune 1991 Pages 403–407https://doi.org/10.1145/127601.127702Online:01 June 1991Publication History 134citation365DownloadsMetricsTotal Citations134Total Downloads365Last 12 Months6Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

The authors consider the state machine language (SML) for describing complex finite state hardware controllers. It provides many of the standard control structures found in modern programming languages. The state tables produced by the SML compiler can be used as input to a temporal logic model checker that can automatically determine whether a specification in the logic CTL is satisfied. The authors describe extensions to SML for the design of modular controllers. These extensions allow a compositional approach to model checking which can substantially reduce its complexity. To demonstrate these methods, the authors discuss the specification and verification of a simple central-processing-unit (CPU) controller.>

The temporal logic model checking algorithm developed by Clarke, Emerson, and Sistla [9] is modified to represent a state graph using binary decision diagrams (BDD's) [4]. Because this representation captures some of the regularity in the state space of sequential circuits with data path logic, we are able to verify circuits with an extremely large number of states. We demonstrate this new technique on a synchronous pipelined design with approximately 5 x 1020 states. Our model checking algorithm handles full CTL with fairness constraints. Consequently, we are able to handle a number of important liveness and fairness properties, which would otherwise not be expressible in CTL. We give empirical results on the performance of the algorithm applied to both synchronous and asynchronous circuits with data path logic.

A parallel algorithm for constructing binary decision diagrams is described. The algorithms treats binary decision graphs as minimal finite automata. The automation for a Boolean function with AND as its main operation (OR operation) is obtained by forming the intersection (union) of the regular sets associated with its operands. The union and intersection operations are implemented by a product construction on the minimal automata for the regular sets. After each product construction step the automaton must be reminimized. The parallel algorithm is designed so that it is possible to find the minimal representations for several Boolean operations in parallel. The level of each operation is determined. Operations at the same level can be performed in parallel without any communication between processors. If there are relatively few operations in one level, then the product generation step is divided into several suboperations and the results are merged.>

A general method that represents the state space symbolically instead of explicitly is described. The generality of the method comes from using a dialect of the mu-calculus as the primary specification language. A model-checking algorithm for mu-calculus formulas which uses R.E. Bryant's (1986) binary decision diagrams to represent relations and formulas symbolically is described. It is then shown how the novel mu-calculus model checking algorithm can be used to derive efficient decision procedures for CTL model checking, satisfiability of linear-time temporal logic formulas, strong and weak observational equivalence of finite transition systems, and language containment of finite omega -automata. This eliminates the need to describe complicated graph-traversal or nested fixed-point computations for each decision procedure. The authors illustrate the practicality of their approach to symbolic model checking by discussing how it can be used to verify a simple synchronous pipeline.>

A parallel resolution theorem prover, called Parthenon, that handles first-order logic is described. Parthenon is apparently the first general-purpose theorem prover to be developed for a multiprocessor. The system is based on a modification of D.H.D. Warren's SRI model (Int. Symp. on Logic Prog., pp.92-101, 1987) for OR-parallelism and implements a variant of D.W. Loveland's (J. ACM, vol.15, pp.236-51, 1968) model elimination procedure. It has been evaluated on various shared memory multiprocessors, including a 16-processor Encore Multimax. The authors have found that typical theorem-proving problems exhibit a great deal of potential parallelism. Parthenon has been able to exploit much of this parallelism, producing both impressive absolute run times and near-linear speed-up curves.>

A method is described for reducing the complexity of temporal logic model checking in systems composed of many parallel processes. The goal is to check properties of the components of a system and then deduce global properties from these local properties. The main difficulty with this type of approach is that local properties are often not preserved at the global level. The authors present a general framework for using additional interface processes to model the environment for a component. These interface processes are typically much simpler than the full environment of the component. By composing a component with its interface processes and then checking properties of this composition, the authors can guarantee that these properties will be preserved at the global level. They give two example compositional systems based on the logic CTL.>

An Escher circuit description is a hierarchical structure composed of cells, wires, connectors between wires, and pins that connect wires to cells. Cells may correspond to primitive circuit elements, or they may be defined in terms of lower level subcells. Unlike other geometrical layout systems, a subcell may be an instance of the cell being defined. When such a recursive cell definition is initiated, the recursion is unwound in a manner reminiscent of the procedure call copy rule in Algol-like programming languages. Cell specifications may have parameters that are used to control the unwinding of recursive cells and to provide for cell families with varying numbers of pins and other internal components. It is shown how the Escher layout system might be used with several nontrivial examples, including a parallel sorting network and a FFT (fast Fourier transform) implementation. The unwinding algorithm is also briefly described.>

An Escher circuit description is a hierarchical structure composed of cells, wires, connectors between wires, and pins that connect wires to cells. Cells may correspond to primitive circuit elements, or they may be defined in terms of lower level subcells. Unlike other geometrical layout systems, a subcell may be instance of the cell being defined. When such a recursive cell definition is instantiated, the recursion is unwound in a manner reminiscent of the procedure call copy rule in Algol-like programming languages. Cell specifications may have parameters that are used to control the unwinding of recursive cells and to provide for cell families with varying numbers of pins and other internal components. We illustrate how the Escher layout system can be used with several nontrivial examples, including a parallel sorting network and a FFT implementation. We also briefly describe the unwinding algorithm.

Article Free Access Share on Reasoning about networks with many identical finite-state processes Authors: E. M. Clarke Carnegie Mellon University, Pittsburgh Carnegie Mellon University, PittsburghView Profile , O. Grumberg Carnegie Mellon University, Pittsburgh Carnegie Mellon University, PittsburghView Profile , M. C. Browne Carnegie Mellon University, Pittsburgh Carnegie Mellon University, PittsburghView Profile Authors Info & Claims PODC '86: Proceedings of the fifth annual ACM symposium on Principles of distributed computingNovember 1986 Pages 240–248https://doi.org/10.1145/10590.10611Online:01 November 1986Publication History 70citation208DownloadsMetricsTotal Citations70Total Downloads208Last 12 Months14Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

Verifying the correctness of sequential circuits has been an important problem for a long time. But lack of any formal and efficient method of verification has prevented the creation of practical design aids for this purpose. Since all the known techniques of simulation and prototype testing are time consuming and not very reliable, there is an acute need for such tools. In this paper we describe an automatic verification system for sequential circuits in which specifications are expressed in a propositional temporal logic. In contrast to most other mechanical verification systems, our system does not require any user assistance and is quite fast—experimental results show that state machines with several hundred states can be checked for correctness in a matter of seconds!

We give an efficient procedure for verifying that a finite-state concurrent system meets a specification expressed in a (propositional, branching-time) temporal logic. Our algorithm has complexity linear in both the size of the specification and the size of the global state graph for the concurrent system. We also show how this approach can be adapted to handle fairness. We argue that our technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite-state concurrent systems. Experimental results show that state machines with several hundred states can be checked in a matter of seconds.

Path expressions were originally proposed by Campbell and Habermann [1] as a mechanism for process synchronization at the monitor level in software. Not unexpectedly, they also provide a useful notation for specifying the behavior of asynchronous circuits. Motivated by this potential application we investigate how to directly translate path expressions into hardware.

The complexity of satisfiability and determination of truth in a particular finite structure are considered for different propositional linear temporal logics. It is shown that these problems are NP-complete for the logic with F and are PSPACE-complete for the logics with F, X, with U, with U, S, X operators and for the extended logic with regular operators given by Wolper.

We give an efficient procedure for verifying that a finite state concurrent system meets a specification expressed in a (propositional) branching-time temporal logic. Our algorithm has complexity linear in both the size of the specification and the size of the global transition graph for the concurrent system. We also show how the logic and our algorithm can be modified to handle fairness. We argue that this technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite state concurrent systems.

In this paper, we view computer networks as distributed systems that provide their users with a set of services, in a way which hides the distinction between those services which are local and those which are remote. We conceive of a given target network configuration as a network of communicating virtual machines and its behavior is modelled by a system of communicating sequential processes. Network protocols are described by a high level concurrent language (CSP) and a methodology is developed which permits the verification of partial and total correctness assertions about the system in a simple and natural way. Global invariants are used to establish invariant properties of the whole system and histories to record the sequence of communication exchanges between every matching pair of processes. Eventuality properties are expressed using linear temporal logic.

For a wtde class of programming languages P and expressive interpretations I, tt is shown that there exist sound and relauvely complete Hoare logics for both partiabcorrectness and termmatton assertions.In fact, under mild assumpUons on P and I it is shown that the assertions true in I are uniformly decidable in the theory of I (Th(I)) fit" the halting problem for P is decidable for fLmte interpretations.Moreover the set of true termination assertions is uniformly recursively enumerable m Th(1) even ff the halting problem for P ~s not dectdable for finite interpretations.Since total-correctness assertions coincide with termination assertions for deterministic programming languages, this last result unexpectedly suggests that good axiom systems for total correctness may exist for a wider spectrum of languages than is the case for partml correctness.

Exchange of information between executing processes is one of the primary reasons for process interaction. Many distributed systems implement explicit message passing primitives to facilitate intercommunication. Typically, a process executes a write command to pass a message to another process, and the target process accepts the message by executing a read command. The semantics of write and read may differ considerably depending on the methods used for storing or buffering messages that have been sent but not yet accepted by the receiving process.

For a wide class of programming languages P and expressive interpretations I, we show that there exist sound and relatively complete Hoare-like logics for both partial correctness and termination assertions. In fact, under mild assumptions on P and I, we show that the assertions true for P in I are uniformly decidable in the theory of I (Th(I)) iff the halting problem for P is decidable for finite interpretations. Moreover termination assertions are uniformly r.e. in Th(I) even if the halting problem for P is not decidable for finite interpretations. Since total correctness assertions coincide with termination assertions for deterministic programming languages, this last result unexpectedly suggests that the class of languages with good axiom systems for total correctness may be wider than for partial correctness.

We consider the complexity of satisfiability and determination of truth in a particular finite structure for different propositional linear temporal logics. We show that both the above problems are NP-complete for the logic with F operator and are PSPACE-complete for the logics with F,X, with U, with U,S,X, and Wolper's extended logic with regular operators [Wo81].

In this paper, we investigate strategies for dynamically reconfiguring shared memory multiprocessor systems that are subject to common memory faults and unpredictable processor deaths. These strategies aim at determining a communication page, i.e., a page of common memory that can be used by a group of processors for storing crucial common resources such as global locks for synchronization and global data structures for voting algorithms. To ensure system reliability, the reconfiguration strategies must be distributed so that each processor independently arrives at exactly the same choice. This type of reconfiguration strategy is currently used in the STAGE operating system on the PLURIBUS multiprocessor [5]. We analyze the weak points of the PLURIBUS algorithm and examine alternative strategies satisfying optimization criteria such as maximization of the number of processors and the number of common memory pages in the reconfigured system. We also present a general distributed algorithm which enables the processors in such a system to exchange the local information that is needed to reach a consensus on system reconfiguration.

Abstract As the cost of processor hardware declines multiprocessor architectures become increasingly cost‐effective and represent an important area for future research. In order to exploit the full potential of multiprocessors, however, it is necessary to understand how to design software which can make effective use of the available parallelism. This paper considers the impact of multiprocessor architecture on the design of high‐level programming languages and, in particular, evaluates the language Ada in the light of the special requirements of realtime multiprocessor systems. We conclude that Ada does not, as currently designed, meet the needs for real‐time embedded systems.

Owicki and Gries have developed a proof system for conditional critical regions . In their system, logically related variables accessed by more than one process are grouped together as resources , and processes are allowed access to a resource only in a critical region for that resource. Proofs of synchronization properties are constructed by devising predicates called resource invariants which describe relationships among the variables of a resource when no process is in a critical region for the resource. In constructing proofs using the system of Owicki and Gries, the programmer is required to supply the resource invariants. Methods are developed in this paper for automatically synthesizing resource invariants. Specifically, the resource invariants of a concurrent program are characterized as least fixpoints of a functional which can be obtained from the text of the program. By the use of this fixpoint characterization and a widening operator based on convex closure, good approximations may be obtained for the resource invariants of many concurrent programs.

Traditional implementations of conditional critical regions and monitors can lead to unproductive "busy waiting" if processes are allowed to wait on arbitrary boolean expressions. Techniques from global flow analysis may be employed at compile time to obtain information about which critical regions (monitor calls) are enabled by the execution of a given critical region (monitor call). We investigate the complexity of computing this information and show how it can be used to obtain efficient scheduling algorithms with less busy waiting.

Owicki and Gries have developed a proof system for conditional critical regions. In their system logically related variables accessed by more than one process are grouped together as resources, and processes are allowed access to a resource only in a critical region for that resource. Proofs of synchronization properties are constructed by devising predicates called resource invariants which describe relationships among the variables of a resource when no process is in a critical region for the resource. In constructing proofs using the system of Owicki and Gries, the programmer is required to supply the resource invariants.We show that convexity plays a key role in the derivation of strong resource invariants. We also develop methods for automatically synthesizing resource invariants. Specifically, we characterize the resource invariants of a concurrent program as least fixpoints of a functional which can be obtained from the text of the program. By using this fixpoint characterization and a widening operator which exploits our observation on the importance of convexity, good approximations may be obtained for the resource invariants of many concurrent programs.

Hoare axiom systems for establishing partial correctness of programs may fail to be complete because of (a) incompleteness of the assertion language relative to the underlying interpretation or (b) inability of the assertion language to express the mvanants of loops Cook has shown that if there IS a complete proof system for the assertion language (l e all true formulas of the assertion language) and if the assertion language satisfies a natural expresstbthty condition then a sound and complete axiom system for a large subset of Algol may be devised We exhibit programming language constructs for which it ms impossible to obtain sound and complete sets of Hoare axioms even in this special sense of Cook's These constructs include (0 recursive procedures with procedure parameters in a programming language which uses static scope of ldenufiers and (u) coroutmes in a language which allows parameterless recurslve procedures Modifications of these constructs for which sound and complete systems of axioms may be obtained are also discussed

We argue that relative soundness and completeness theorems for Floyd-Hoare Axiom Systems ([6], [5], [18]) are really fixed point theorems. We give a characterization of program invariants as fixed points of functionals which may be obtained in a natural manner from the text of a program. We show that within the framework of this fixed point theory, relative soundness and completeness results have a particularly simple interpretation. Completeness of a Floyd-Hoare Axiom system is equivalent to the existence of a fixed point for an appropriate functional, and soundness follows from the maximality of this fixed point, The functionals associated with regular procedure declarations are similar to predicate transformers of Dijkstra; for non-regular recursions it is necessary to use a generalization of the predicate transformer concept which we call a relational transformer.

Hoare-like deduction systems for establishing partial correctness of programs may fail to be complete because of (a) incompleteness of the assertion language relative to the underlying interpretation or (b) inability of the assertion language to express the invariants of loops. S. Cook has shown that if there is a complete proof system for the assertion language (e.g. all true statements of the assertion language) and if the assertion language satisfies a certain natural expressibility condition, then sound and complete axiom systems for a fairly large subset of Algol may be devised. We exhibit programming language constructs for which it is impossible to obtain sound and complete sets of Hoare-like axioms even in this special sense of Cook's. These constructs include (i) recursive procedures with procedure parameters in a programming language which uses static scope of identifiers and (ii) coroutines in a language which allows parameterless recursive procedures. Modifications of these constructs for which it is possible to obtain sound and complete systems of axioms are also discussed.