Program logics are formal systems for specifying and reasoning about software programs. Most program logics make the strong assumption that all threads agree on the value of shared memory at all times. This assumption can be unsound though for programs with races, like many concurrent data structures. Verification of these difficult programs must take into account the weaker models of memory provided by the architectures on which they execute. In this paper, we describe progress toward a program logic for local reasoning about racy concurrent programs executing on a weak, x86-like memory model.

A Concurrent Kleene Algebra offers two composition operators, one that stands for sequential execution and the other for concurrent execution. In this paper we investigate the abstract background of this law in terms of independence relations on which a concrete trace model of the algebra is based. Moreover, we show the interdependence of the basic properties of such relations and two further laws that are essential in the application of the algebra to a Jones style rely/guarantee calculus. Finally we reconstruct the trace model in a more abstract setting based on the notion of atoms from lattice theory.

A concurrent Kleene algebra offers, next to choice and iteration, operators for sequential and concurrent composition, related by an inequational form of the exchange law. We show applicability of the algebra to a partially-ordered trace model of program execution semantics and demonstrate its usefulness by validating familiar proof rules for sequential programs (Hoare triples) and for concurrent ones (Jones's rely/guarantee calculus). This involves an algebraic notion of invariants; for these the exchange inequation strengthens to an equational distributivity law. Most of our reasoning has been checked by computer.

In this paper, we present a trace semantics based on graphs: nodes represent the events of a program's execution, and edges represent dependencies among the events. The style is reminiscent of partially ordered models, though we do not generally require properties like transitivity or acyclicity. Concurrency and sequentiality are defined using variations on separating conjunctions, which are instances of model theories of separation logic and bunched logic. The model has pleasant algebraic properties, which are shown with surprisingly simple proofs. We present a number of theorems about the generic model, including the soundness of the laws of Hoare logic and the Jones rely/guarantee calculus. No particular languages or applications are studied in the paper; we leave this to future work.

Orc is a language for structured concurrent programming. Expressions in an Orc program are either primitive, or a combination of two expressions. A primitive expression calls an existing service, a site, which performs its computations and returns a result. There are only three combinators for Orc expressions, which allow sequential and concurrent executions of expressions, and concurrent execution with termination.

Orc is particularly well-suited for task orchestration, a form of concurrent programming with applications in workflow, business process management, and web service orchestration. Orc provides constructs to orchestrate the concurrent invocation of services while managing time-outs, priorities, and failures of services or communication.

Previous work on the semantics of Orc has treated only its asynchronous behavior. The inclusion of time or the effect of delay on a computation has not yet been modeled. In this paper, we define a relative-time operational semantics of Orc that allows reasoning about delays, which are introduced explicitly by time-based constructs or implicitly by network delays. We develop a number of identities among Orc expressions and define an equality relation that is a congruence. For the simpler case of asynchronous semantics without time, we develop additional results about monotonicity and continuity of the Orc combinators, which are used to assign meanings to recursive Orc programs.

Long-running distributed applications that automate critical decision processes require Byzantine fault tolerance to ensure progress in spite of arbitrary failures. Existing replication protocols for data servers guarantee that externally requested operations execute correctly even if a bounded number of replicas fail arbitrarily. However, since these protocols only support passive state machine replication, they are insufficient to support continued correct execution of autonomous long-running distributed applications.

Building on the Castro and Liskov Byzantine Fault Tolerance protocol for replicated state machines (CLBFT), we present a practical algorithm for Byzantine fault-tolerant execution of autonomous distributed applications. The algorithm supports replicated clients that actively execute application logic by issuing operation requests on replicated data servers as well as other replicated clients. Our work facilitates dynamic upgrades to replica groups, supports both synchronous and asynchronous operation requests, and provides fault isolation between replica groups with respect to both correctness and performance. The algorithm scales well to large replica groups with only twice the latency and message complexity as compared to CLBFT, which supports only unreplicated clients.

A Knuth-Bendix completion procedure is parametrized by a reduction ordering used to ensure termination of intermediate and resulting rewriting systems. While in principle any reduction ordering can be used, modern completion tools typically implement only Knuth-Bendix and path orderings. Consequently, the theories for which completion can possibly yield a decision procedure are limited to those that can be oriented with a single path order.

In this paper, we present a variant on the Knuth-Bendix completion procedure in which no ordering is assumed. Instead we rely on a modern termination checker to verify termination of rewriting systems. The new method is correct if it terminates; the resulting rewrite system is convergent and equivalent to the input theory. Completions are also not just ground-convergent, but fully convergent. We present an implementation of the new procedure, Slothrop, which automatically obtains such completions for theories that do not admit path orderings.

Dependent types have been proposed for functional programming languages as a means of expressing semantically rich properties as types. In this paper, we consider the problem of bringing semantic programming based on dependent types to an object-oriented language. A type-theoretically light extension to Java (with generics) is proposed, called property types. These are types indexed not by other types (as in Java with generics) but by immutable expressions. We consider programming with two examples of property types: a property type HasFactors<long x, Set a>, expressing that the elements of a are the multiplicative factors of x; and a property type Sorted<List l>, expressing that l is sorted.

In this paper a language-based approach to functionally correct imperative programming is proposed. The approach is based on a programming language called RSP1, which combines dependent types, general recursion, and imperative features in a type-safe way, while preserving decidability of type checking. The methodology used is that of internal verification, where programs manipulate programmer-supplied proofs explicitly as data. The fundamental technical idea of RSP1 is to identify problematic operations as impure, and keep them out of dependent types. The resulting language is powerful enough to verify statically non-trivial properties of imperative and functional programs. The paper presents the ideas through the examples of statically verified merge sort, statically verified imperative binary search trees, and statically verified directed acyclic graphs.

The problem of obtaining small conflict clauses in SMT systems has received a great deal of attention recently. We report work in progress to find small subsets of the current partial assignment that imply the goal formula when it has been propositionally simplified to a boolean value. The approach used is algebraic proof mining. Proofs from a propositional reasoner that the goal is equivalent to a boolean value (in the current assignment) are viewed as first-order terms. An equational theory between proofs is then defined, which is sound with respect to the quasi-order “proves a more general set theorems.” The theory is completed to obtain a convergent rewrite system that puts proofs into a canonical form. While our canonical form does not use the smallest subset of the current assignment, it does drop many unnecessary parts of the proof. The paper concludes with discussion of the complexity of the problem and effectiveness of the approach.

Program logics are formal logics designed to facilitate specification and correctness reasoning for software programs. Separation logic, a recent program logic for C-like programs, has found great success in automated verification due in large part to its embodiment of the principle of local reasoning, in which specifications and proofs are restricted to just those resources—variables, shared memory addresses, locks, etc.—used by the program during execution.

Existing program logics make the strong assumption that all threads agree on the values of shared memory at all times. But, on modern computer architectures, this assumption is unsound for certain shared-memory concurrent programs: namely, those with races. Typically races are considered to be errors, but some programs, like lock-free concurrent data structures, are necessarily racy. Verification of these difficult programs must take into account the weaker models of memory provided by the architectures on which they execute.

This dissertation project seeks to explicate a local reasoning principle for x86-like architectures. The principle is demonstrated with a new program logic for concurrent C-like programs that incorporates ideas from separation logic. The goal of the logic is to allow verification of racy programs like concurrent data structures for which no general-purpose high-level verification techniques exist.

Program logics are formal logics designed to facilitate specification and correctness reasoning for software programs of a particular programming language. Separation logic, a new program logic for C-like pointer programs, has found great success due in large part to its embodiment of a local reasoning principle, in which specifications and proofs are restricted to just those resources---variables, shared memory addresses, locks---used by the program during execution.

Existing program logics make the strong assumption that all threads agree on the value of shared memory at all times. This assumption is unsound, though, for shared-memory concurrent programs with race conditions, like concurrent data structures. Verification of these difficult programs must take into account the weaker models of memory provided by the architectures on which they execute.

In my dissertation project, I explicate a local reasoning principle for a weak memory model based on a formal specification of the x86 multiprocessor memory model. I demonstrate this principle with a new program logic for fine-grained concurrent C-like programs that incorporates ideas from separation logic and rely/guarantee. Notably, the logic may be applied soundly to programs with races, for which no general high-level verification techniques exist.

A sequential program logic based on separation logic is defined and proved sound w.r.t. a weak x86-like memory model.

Orc is a language for structured concurrent programming. Orc provides three powerful combinators that define the structure of a concurrent computation. These combinators support sequential and concurrent execution, and concurrent execution with blocking and termination.

Orc is particularly well-suited for task orchestration, a form of concurrent programming with applications in workflow, business process management, and web service orchestration. Orc provides constructs to orchestrate the concurrent invocation of services while managing time-outs, priorities, and failures of services or communication.

Previous work on the semantics of Orc has focused on its asynchronous behavior. In this report, we define a relative-time operational semantics of Orc that allows reasoning about delays, which are introduced explicitly by time-based constructs or implicitly by network delays. We develop a number of identities among Orc expressions and define an equality relation that is a congruence. We also develop a denotational semantics for Orc, in which the meaning of an Orc expression is a set of traces. A number of properties about the semantics are shown here, including equivalence of the operational and denotational semantics.

Knuth-Bendix completion is a technique for equational automated theorem proving based on term rewriting. This classic procedure is parametrized by an equational theory and a (well-founded) reduction order used at runtime to ensure termination of intermediate rewriting systems. Any reduction order can be used in principle, but modern completion tools typically implement only a few classes of such orders (e.g., recursive path orders and polynomial orders). Consequently, the theories for which completion can possibly succeed are limited to those compatible with an instance of an implemented class of orders. Finding and specifying a compatible order, even among a small number of classes, is challenging in practice and crucial to the success of the method.

In this thesis, a new variant on the Knuth-Bendix completion procedure is developed in which no order is provided by the user. Modern termination-checking methods are instead used to verify termination of rewriting systems. We prove the new method correct and also present an implementation called Slothrop which obtains solutions for theories that do not admit typical orders and that have not previously been solved by a fully automatic tool.

Byzantine agreement protocols for replicated deterministic state machines guarantee that externally requested operations continue to execute correctly even if a bounded number of replicas fail in arbitrary ways. The state machines are passive, with clients responsible for any active ongoing application behavior. However, the clients are unreplicated and outside the fault-tolerance boundary. Consequently, agreement protocols for replicated state machines do not guarantee continued correct execution of long-running client applications.

Building on the Castro and Liskov Byzantine Fault Tolerance protocol for unreplicated clients (CLBFT), we present a practical algorithm for Byzantine fault-tolerant execution of long-running distributed applications in which replicated deterministic clients invoke operations on replicated deterministic servers. The algorithm scales well to large replica groups, with roughly double the latency and message count when compared to CLBFT, which supports only unreplicated clients. The algorithm supports both synchronous and asynchronous clients, provides fault isolation between client and server groups with respect to both correctness and performance, and uses a novel architecture that accommodates externally requested software upgrades for long-running evolvable client applications.

In this paper a language-based approach to functionally correct imperative programming is proposed. The approach is based on a programming language called RSP1, which combines dependent types, general recursion, and imperative features in a type-safe way, while preserving decidability of type checking. The methodology used is that of internal verification, where programs manipulate programmer-supplied proofs explicitly as data. The fundamental technical idea of RSP1 is to identify problematic operations as impure, and keep them out of dependent types. The resulting language is powerful enough to verify statically non-trivial properties of imperative and functional programs. The paper presents the ideas through the examples of statically verified merge sort, statically verified imperative binary search trees, and statically verified directed acyclic graphs.