The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrency

Program logics and semantics tell a pleasant story about sequential composition: when executing (S1;S2), we first execute S1 then S2. To improve performance, however, processors execute instructions out of order, and compilers reorder programs even more dramatically. By design, single-threaded systems cannot observe these reorderings; however, multiple-threaded systems can, making the story considerably less pleasant. A formal attempt to understand the resulting mess is known as a “relaxed memory model.” Prior models either fail to address sequential composition directly, or overly restrict processors and compilers, or permit nonsense thin-air behaviors which are unobservable in practice. To support sequential composition while targeting modern hardware, we enrich the standard event-based approach with preconditions and families of predicate transformers. When calculating the meaning of (S1; S2), the predicate transformer applied to the precondition of an event e from S2 is chosen based on the set of events in S1 upon which e depends. We apply this approach to two existing memory models.

Inputs, Outputs, and Composition in the Logic of Information Flows

The logic of information flows (LIF) is a general framework in which tasks of a procedural nature can be modeled in a declarative, logic-based fashion. The first contribution of this paper is to propose semantic and syntactic definitions of inputs and outputs of LIF expressions. We study how the two relate and show that our syntactic definition is optimal in a sense that is made precise. The second contribution of this paper is a systematic study of the expressive power of sequential composition in LIF. Our results on composition tie in the results on inputs and outputs, and relate LIF to first-order logic (FO) and bounded-variable LIF to bounded-variable FO.

A Parametrized Analysis of Algorithms on Hierarchical Graphs

Hierarchical graphs are used in order to describe systems with a sequential composition of sub-systems. A hierarchical graph consists of a vector of subgraphs. Vertices in a subgraph may “call” other subgraphs. The reuse of subgraphs, possibly in a nested way, causes hierarchical graphs to be exponentially more succinct than equivalent flat graphs. Early research on hierarchical graphs and the computational price of their succinctness suggests that there is no strong correlation between the complexity of problems when applied to flat graphs and their complexity in the hierarchical setting. That is, the complexity in the hierarchical setting is higher, but all “jumps” in complexity up to an exponential one are exhibited, including no jumps in some problems. We continue the study of the complexity of algorithms for hierarchical graphs, with the following contributions: (1) In many applications, the subgraphs have a small, often a constant, number of exit vertices, namely vertices from which control returns to the calling subgraph. We offer a parameterized analysis of the complexity and point to problems where the complexity becomes lower when the number of exit vertices is bounded by a constant. (2) We describe a general methodology for algorithms on hierarchical graphs. The methodology is based on an iterative compression of subgraphs in a way that maintains the solution to the problems and results in subgraphs whose size depends only on the number of exit vertices, and (3) we handle labeled hierarchical graphs, where edges are labeled by letters from some alphabet, and the problems refer to the languages of the graphs.

Autonomous Stairwell Ascent

SummaryThis paper documents autonomous multi-floor stairwell ascent by a legged robot. This is made possible through empirically deployed sequential composition of several reactive controllers, with perceptually triggered transitions. This composition relies on simplified assumptions regarding the robot’s sensory capabilities, its level of mobility, and the environment it operates in. The discrepancies between these assumptions and the physical reality are capably handled by the intrinsic motor competence of the robot. This behavior is implemented on the legged RHex platform and experiments spanning 10 different stairwells with various challenges are conducted.

Feedback motion planning of unmanned surface vehicles via random sequential composition

In this paper, we propose a new motion planning method that aims to robustly and computationally efficiently solve path planning and navigation problems for unmanned surface vehicles (USVs). Our approach is based on synthesizing two different existing methodologies: sequential composition of dynamic behaviours and rapidly exploring random trees (RRT). The main motivation of this integrated solution is to develop a robust feedback-based and yet computationally feasible motion planning algorithm for USVs. In order to illustrate the main approach and show the feasibility of the method, we performed simulations and tested the overall performance and applicability for future experimental applications. We also tested the robustness of the method under relatively extreme environmental uncertainty. Simulation results indicate that our method can produce robust and computationally feasible solutions for a broad class of USVs.