In this paper, we study the problem of incremental maintenance of Datalog programs and model it as a scheduling problem on DAGs. We design provably good time- and memory-efficient scheduling algorithms for (re)executing a Datalog program where some (but not necessarily all) of the inputs have changed. We prove that our schedulers, called LevelBased and LevelBased with lookahead, have asymptotically improved running time and space efficiency when compared with benchmark algorithms used in production at LogicBlox.The main result of the paper is a hybrid scheduler, which combines LevelBased with the production LogicBlox scheduler (or any other heuristic scheduler). The hybrid scheduler achieves strong worst-case guarantees and robustness without losing out on the best-case behavior of the production LogicBlox scheduler. Our experiments show that the hybrid scheduler results in similar or improved total execution times compared to LogicBlox scheduler, while consistently reducing the scheduling overhead-by as much as 50% on some datasets. This hybrid scheme requires little to no overhead but provides predictability and reliability, which are crucial in a commercial application such as LogicBlox.

As a bridge from informal business requirements to precise specifications, conceptual models serve a critical role in the development of enterprise systems. Instantiating conceptual models with test data can help stakeholders validate the model and provide developers with a test database to validate their code. ORM is a popular conceptual modeling language due in part to its expressive constraint language. Due to that expressiveness, instantiating an arbitrary ORM model is NP-hard. Smaragdakis et al. identified a subset of ORM called ORM− that can be instantiated in polynomial time. However, ORM− excludes several constraints commonly used in commercial models. Recent research has extended ORM− through semantics-preserving transformations. We extend the set of ORM models that can be transformed to ORM− models by using a class of non-semantics-preserving transformations called constraint strengthening. We formalize our approach as a special case of Stevens’ model transformation framework. We discuss an example transformation and its limitations, and we conclude with a proposal for future research.

Conceptual data models describe information systems without the burden of implementation details, and are increasingly used to generate code. They could also be analyzed for consistency and to generate test data except that the expressive constraints supported by popular modeling notations make such analysis intractable. In an earlier empirical study of conceptual models created at LogicBlox Inc., Smaragdakis, Csallner, and Subramanian found that a restricted subset of ORM, called ORM−, includes the vast majority of constraints used in practice and, moreover, allows scalable analysis. After that study, however, LogicBlox Inc. obtained a new ORM modeling tool, which supports discovery and specification of more complex constraints than the previous tool. We report findings of a follow-up study of models constructed using the more powerful tool. Our study finds that LogicBlox developers increasingly rely on a small number of features not in the ORM− subset. We extend ORM− with support for two of them: objectification and a restricted class of external uniqueness constraints. The extensions significantly improve our ability to analyze the ORM models created by developers using the new tool. We also show that a recent change to ORM has rendered the original ORM− algorithms unsound, in general; but that an efficient test suffices to show that these algorithms are in fact sound for the ORM− constraints appearing in any of the models currently in use at LogicBlox.

Concurrent software is notoriously difficult to debug. We investigate the use of UML sequence diagrams to help developers correctly reason about the potential behaviors of buggy concurrent software. We conducted a controlled experiment that compared internal (i.e., "in the head") and external representations for reasoning about multithreaded software. For external representations, participants created multithreaded sequence diagrams. The results of the experiment demonstrate a strong positive effect associated with using external representations. Participants who drew diagrams were significantly more successful at reasoning about the potential behavior of concurrent software. Moreover, participants who produced diagrams with higher levels of detail and with fewer errors tended to achieve greater levels of success. Additionally, this paper contributes an extension to the UML sequence diagram notation for showing behavior of multithreaded software and formal metrics for assessing the complexity of thread interactions.

We describe a framework, called the synchronization policy prototyper (SyPP), for generating tools to aid in assessing the appropriateness of strictly exclusive synchronization policies under expected program usage scenarios. A SyPP tool aims to help during evolution of an existing program when the synchronization policy that it implements needs to be changed.

Empirical studies are important for understanding how well current design methods and notations support development of multi-threaded programs. Unfortunately, concurrency exacerbates an already difficult problem in drawing conclusions from such studies: How to objectively measure the quality of candidate solutions produced by participants in the studies. This paper explores the use of formal modeling and analysis for this purpose. We describe initial findings of a small pilot study to determine if we can objectively differentiate sample candidate solutions with respect to their use of synchronization primitives. To do so, we faithfully model these candidate solutions and various synchronization-related properties in the Finite State Processes (FSP) notation and use the Labeled Transition System Analyzer (LTSA) to analyze the solution models against the properties.

Graduates of computer science degree programs are increasingly being asked to maintain large, multi-threaded software systems; however, the maintenance of such systems is typically not well-covered by software engineering texts or curricula. We conducted a think-aloud study with 15 students in a graduate-level computer science class to discover the strategies that students apply, and to what effect, in performing corrective maintenance on concurrent software. We collected think-aloud and action protocols, and annotated the protocols for a number of behavioral attributes and maintenance strategies. We divided the protocols into groups based on the success of the participant in both diagnosing and correcting the failure. We evaluated these groups for statistically significant differences in these attributes and strategies.

While the sources of complexity in the initial design and verification of multi-threaded software systems are well-documented, less is known of the issues specific to the maintenance of these systems. The literature contains a number of observational studies of programmers performing maintenance, conducted in the context of sequential software and designed to investigate the factors and behaviors that lead to success. To help fill the gap in knowledge in the area of concurrent software maintenance, we conducted a study that refines the findings of two prior studies, those of Littman et al. and of Vessey, to address issues and obstacles that arise in the understanding of concurrent software. We validated these refinements by observing programmers performing corrective maintenance on a small but complex multi-threaded server program.

It is generally accepted that concurrency can be difficult for students to reason about. While some studies provide insight into the nature of these difficulties [6], work remains to be done in understanding the aspects of learning about concurrency that are most difficult, and in developing approaches to dealing with this problem. We have conducted instructor interviews and an observational study of students, identified several key difficulties that students encounter, and developed a diagram that we believe will be an aid to understanding and problem-solving. We present the diagram and results of an initial user evaluation.

The field of program comprehension is characterized by both the continuing development of new tools and techniques and the adaptation of existing techniques to address program comprehension needs for new software development and maintenance scenarios. The adoption of these techniques and tools in industry requires proper experimentation to assess the advantages and disadvantages of each technique or tool and to let the practitioners choose the most suitable approach for a specific problem. The objective of this working session is to encourage researchers and practitioners working in the area of program comprehension to join forces to design and carry out studies related to program comprehension, including observational studies, controlled experiments, case studies, surveys, and contests, and to develop standards for describing and carrying out such studies in a way that facilitates replication of data and aggregation of the results of related studies.

Programs that use multithreaded concurrency are known to be difficult to design. Moreover, research in computer-science education suggests that concurrency and synchronization concepts are generally difficult to master. It stands to reason that comprehension tasks may be more complex for programs that employ concurrency than for sequential programs. We believe that external representations, specifically refinements to some of the popular UML modeling notations, should aid students in mastering fundamental concurrency/synchronization concepts and should enable practitioners to better comprehend the dynamically evolving nature of the these programs. In this paper, we present our synchronization adorned UML (saUML) sequence diagram notation that highlights aspects of thread interactions and describe an empirical study of whether these diagrams, as opposed to purely textual representations, help students to better understand concurrent executions and concurrency concepts, as measured by their ability to answer questions about a particular execution of a multi-threaded system. A statistically significant benefit was found from the study.

This paper explores an approach to design for verification in systems built atop a middleware framework which separates synchronization concerns from the "core-functional logic" of a program. The framework is based on a language-independent compositional model of synchronization contracts, called Szumo, which integrates well with popular OO design artifacts and provides strong guarantees of non-interference for a class of strictly exclusive systems. An approach for extracting models from Szumo design artifacts and analyzing the generated models to detect deadlocks is described. A key decision was to use Constraint Handling Rules to express the semantics of synchronization contracts, which allowed a transparent model of the implementation logic.

It is widely held that programming language extensions that support separation of concerns and that are also integrative benefit development, maintenance and reuse of software designs and code. Such is the intent of our synchronization units model (Szumo), which unifies new features for expressing synchronization in a multi-threaded program with existing features of an object-oriented language. However, to make effective use of a language extension, a programmer needs an accurate mental model of how new concepts affect and are affected by existing concepts. Moreover, good separation dictates that interactions between these concepts should be understandable at the level of the new concepts. This suggests that the semantics of Szumo should be specifiable as a self-contained partial specification, called a view, and the semantics of its integration with other language features should be specifiable by view composition. To our knowledge, however, view-based approaches have not been applied in specifying the semantics of language extensions. Moreover, devising separable views that serve to simplify comprehensibility of a complex specification is still more of an art than a science. This paper presents a case study in the use of views in structuring a Z specification of Szumo

The safe and reliable use of concurrency in multi-threaded systems has emerged as a fundamental engineering concern. We recently developed a model of synchronization contracts to address this concern in programs written in object-oriented languages. Programs written using our model comprise modules that declare access requirements in module interfaces in lieu of using low-level synchronization primitives in module implementations. At run time, these contracts are negotiated to derive schedules that guarantee freedom from data races while avoiding a large class of deadlock situations

Recently, there has been growing interest in formalizing UML, thereby enabling rigorous analysis of its many graphical diagrams. Two obstacles currently limit the adoption and use of UML formalizations in practice. First is the need to verify the consistency of artifacts under formalization. Second is the need to validate formalization approaches against domain-specific requirements. Techniques from the emerging field of requirements traceability hold promise for addressing these obstacles. This paper contributes a technique called retrieval by construction (RBC), which establishes traceability links between a UML model and a target model intended to denote its semantics under formalization. RBC provides an approach for structuring and representing the complex one-to-many links that are common between UML and target models under formalization. RBC also uses the notion of value identity in a novel way that enables the specification of the link-retrieval criteria using generative procedures. These procedures are a natural means for specifying UML formalizations. We have validated the RBC technique in a tool framework called UBanyan, written in C++. We applied the tool to three case studies, one of which was obtained from the industry. We have also assessed our results using the two well-known traceability metrics: precision and recall. Preliminary investigations suggest that RBC can be a useful traceability technique for validating and verifying UML formalizations.

Amalia is a generator framework for constructing analyzers for operationally defined formal notations. These generated analyzers are components that are designed for customization and integration into a larger environment. The customizability, and efficiency of Amalia analyzers owe to a computational structure called an inference graph. This paper describes this structure, how inference graphs enable Amalia to generate analyzers for operational specifications, and how we build in assurance. On another level, this paper illustrates how to balance the need for assurance, which typically implies a formal proof obligation, against other design concerns, whose solutions leverage design techniques that are not (yet) accompanied by mature proof methods. We require Amalia-generated designs to be transparent with respect to the formal semantic models upon which they are based. Inference graphs are complex structures that incorporate many design optimizations. While not formally verifiable, their fidelity with respect to a formal operational semantics can be discharged by inspection.

The Amalia framework generates lightweight components that automate the analysis of operational specifications and designs. A key concept is the step analyzer, which enables Amalia to automatically tailor high-level analyses, such as behavior simulation and model checking, to different specification languages and representations. A step analyzer uses a new abstraction, called an inference graph, for the analysis. It creates and evaluates an inference graph on-the-fly during a top-down traversal of a specification to deduce the specification's local behaviors (called steps). The nodes of an inference graph directly reify the rules in an operational semantics, enabling Amalia to automatically generate a step analyzer from an operational description of a notation's semantics. Inference graphs are a clean abstraction that can be formally defined. The paper provides a detailed but informal introduction to inference graphs. It uses example specifications written in LOTOS for purposes of illustration.

Automatic-verification capability tends to be packaged into stand-alone tools, as opposed to components that are easily integrated into a larger software-development environment. Such packaging complicates integration because it involves translating internal representations into a form compatible with the stand-alone tool. By contrast, lightweight-analysis components package analysis capability in a form that does not involve such a translation. Borrowing ideas from GenVoca and object-oriented design patterns, we developed a domain model and an automatic generation framework for lightweight-analysis components. The generated components operate directly over the internal form of a specification without requiring a change in representation. Moreover, the domain model identifies several "useful subsets" that can be used to customize analysis capability to a particular application. We validated this domain model by generating lightweight analyzers for temporal logic and the behavioral subset of Lotos.

Reverse engineering a program constructs a high-level representation suitable for various software development purposes such as documentation or reengineering. Unfortunately however, there are no established guidelines to assess the adequacy of such a representation. We propose two such criteria, completeness and accuracy, and show how they can be determined during the course of reversing the representation. A representation is successfully reversed when it is given as input to a suitable code generator, and a program equivalent to the original is produced. To explore this idea, we reverse engineer a small but complex numerical application, represent our understanding using algebraic specifications, and then use a code generator to produce code from the specification. We discuss the strengths and weaknesses of the approach as well as alternative approaches to reverse engineering adequacy.

We present the universe model, a new approach to concurrency management that isolates concurrency concerns and represents them in the modular interface of a component. This approach improves program comprehension, module composition, and reliability for concurrent systems. The model is founded on designer-specified invariant properties, which declare a component's dependencies on other concurrent components. Process scheduling is then automatically derived from these invariants. We illustrate the advantages of this approach by applying it to a real-world example.

Direct-manipulation user interfaces are difficult to implement as a tapered hierarchy. Features such as drag enabling and continuous graphical feedback require frequent interaction and collaboration among a large number of objects in multiple layers. These collaborations complicate the design of the interfaces in the various layers. We present a new component-interface model called a "mode component", whose features simplify the expression of collaboration enabling and feedback across layer boundaries. We illustrate the use of mode components through a large example.

Automated user-interface generation environments have been criticized for their failure to deliver rich and powerful interactive applications. To specify more powerful systems, designers require multiple specialized modeling notations. The model-composition problem is concerned with automatically deriving powerful, correct, and efficient user interfaces from multiple models specified in different notations. Solutions balance the advantages of separating code generation into specialized code generators with deep, model-specific knowledge against the correctness and efficiency obstacles that result from such separation. We present a correct and efficient solution that maximizes the advantage of separation through run-time composition mechanisms.

The various goals and requirements of a system are realized in software as fragments of code that are typically "interleaved" in that they may be woven together in the same contiguous textual area of code. The fragments of code are often delocalized and overlap rather than being composed in a simple linear sequence. Interleaving severely complicates software comprehension and maintenance. To address this problem, we are developing analysis tools, based on the Software Refinery. This paper describes our experiences in detecting interleaving in a corpus of mathematical software written in Fortran from the Jet Propulsion Laboratory. In particular, it discusses how feasible it is to detect interleaving of various types and the ability of existing tools to assist these types of detection.

Dependenceanalysis is critical to tools for parallel programming such as compilers, parallelizers, and performance analyzers.Conventional algorithms and data structures for dependence analysis are complex and time consuming, requiring multiple passes.In addition, these algorithms cannot easily be adapted to incrementally recompute dependence after program modifications.In this paper we present a new approach to dependence analysis which computes dependence in linear time (no backtracking) with a low space overhead.The algorithm handles arbitrary, unstructured control flow and calls to subprograms whose dependence have not been analyzed, and can be extended to allow very rapid incremental dependence recomputation.The algorithms are currently being implemented in PAT, a portable parallelization tool.

Incrementally updating dependence information during interactive parallelization is a difficult proposition. We have developed a tool (PAT) that maintains dependence information during incremental transformations to a Fortran program, including loop parallelization, code replication, alignment and shifting, as well as insertion and deletion of code including parallel primitives. Our analysis is based on a variation on the standard approach to dependence graph generation, with program wide and local information separated in a sequential and a parallel dependence graph.