Substructural type systems provide the ability to speak about resources . By enforcing usage restrictions on inputs to computations they allow programmers to reify limited system units–such as memory–in types. We demonstrate a new form of resource reasoning founded on constraining outputs and explore its utility for practical programming. In particular, we identify a number of disparate programming features explored largely in the security literature as various fragments of our unified framework. These encompass capabilities, quantitative information leakage, sandboxing in the style of the Linux seccomp interface, authorization protocols, and more. We furthermore explore its connection to conventional input-based resource reasoning, casting it as an internal treatment of the constructive Kripke semantics of substructural logics. We verify the capability, quantity, and protocol safety of our system through a single logical relations argument. In doing so, we take the first steps towards obtaining the ultimate multitool for security reasoning.

This paper explores the integration of Visual Code Assistants in Integrated Development Environments (IDEs). In Software Engineering, whiteboard sketching is often the initial step before coding, serving as a crucial collaboration tool for developers. Previous studies have investigated patterns in SE sketches and how they are used in practice, yet methods for directly using these sketches for code generation remain limited. The emergence of visually-equipped large language models presents an opportunity to bridge this gap, which is the focus of our research. In this paper, we built a first prototype of a Visual Code Assistant to get user feedback regarding in-IDE sketch-to-code tools. We conduct an experiment with 19 data scientists, most of whom regularly sketch as part of their job. We investigate developers' mental models by analyzing patterns commonly observed in their sketches when developing an ML workflow. Analysis indicates that diagrams were the preferred organizational component (52.6%), often accompanied by lists (42.1%) and numbered points (36.8%). Our tool converts their sketches into a Python notebook by querying an LLM. We use an LLM-as-judge setup to score the quality of the generated code, finding that even brief sketching can effectively generate useful code outlines. We also find a positive correlation between sketch time and the quality of the generated code. We conclude the study by conducting extensive interviews to assess the tool's usefulness, explore potential use cases, and understand developers' needs. As noted by participants, promising applications for these assistants include education, prototyping, and collaborative settings. Our findings signal promise for the next generation of Code Assistants to integrate visual information, both to improve code generation and to better leverage developers' existing sketching practices.

Developers rely on the static safety guarantees of the Rust programming language to write secure and performant applications. However, Rust is frequently used to interoperate with other languages which allow design patterns that conflict with Rust's evolving aliasing models. Miri is currently the only dynamic analysis tool that can validate applications against these models, but it does not support finding bugs in foreign functions, indicating that there may be a critical correctness gap across the Rust ecosystem. We conducted a large-scale evaluation of Rust libraries that call foreign functions to determine whether Miri's dynamic analyses remain useful in this context. We used Miri and an LLVM interpreter to jointly execute applications that call foreign functions, where we found 46 instances of undefined or undesired behavior in 37 libraries. Three bugs were found in libraries that had more than 10,000 daily downloads on average during our observation period, and one was found in a library maintained by the Rust Project. Many of these bugs were violations of Rust's aliasing models, but the latest Tree Borrows model was significantly more permissive than the earlier Stacked Borrows model. The Rust community must invest in new, production-ready tooling for multi-language applications to ensure that developers can detect these errors.

Liquid types can express richer verification properties than simple type systems. However, despite their advantages, liquid types have yet to achieve widespread adoption. To understand why, we conducted a study analyzing developers’ challenges with liquid types, focusing on LiquidHaskell. Our findings reveal nine key barriers that span three categories, including developer experience, scalability challenges with complex and large codebases, and understanding the verification process. Together, these obstacles provide a comprehensive view of the usability challenges to the broader adoption of liquid types and offer insights that can inform the current and future design and implementation of liquid type systems.

Information flow control is a long-studied approach for establishing non-interference properties of programs. For instance, it can be used to prove that a secret does not interfere with some computation, thereby establishing that the former does not leak through the latter. Despite their potential as a holy grail for security reasoning and their maturity within the literature, information flow type systems have seen limited adoption. In practice, information flow specifications tend to be excessively complex and can easily spiral out of control even for simple programs. Additionally, while non-interference is well-behaved in an idealized setting where information leakage never occurs, most practical programs must violate non-interference in order to fulfill their purpose. Useful information flow type systems in prior work must therefore contend with a definition of non-interference extended with declassification, which often offers weaker modular reasoning properties. We introduce structural information flow, which both illuminates and addresses these issues from a logical viewpoint. In particular, we draw on established insights from the modal logic literature to argue that information flow reasoning arises from hybrid logic, rather than conventional modal logic as previously imagined. We show with a range of examples that structural information flow specifications are straightforward to write and easy to visually parse. Uniquely in the structural setting, we demonstrate that declassification emerges not as an aberration to non-interference, but as a natural and unavoidable consequence of sufficiently general machinery for information flow. This flavor of declassification features excellent local reasoning and enables our approach to account for real-world information flow needs without compromising its theoretical elegance. Finally, we establish non-interference via a logical relations approach, showing off its simplicity in the face of the expressive power captured.

The reactive programming paradigm has become ubiquitous for modern web and mobile app development. But despite its many benefits, today reactive programming is limited to data updates within the client, leaving to the programmer the tedious and error-prone tasks of managing updates to code and synchronizing data updates between reactive clients and a server database. In this paper, we lay out the vision for Meerkat, a tierless, reactive, and live programming language designed to scale to the needs of modern applications. We introduce the language through a chat application which runs on our prototype implementation. We then describe approaches for modularizing and scaling Meerkat programs, customizing tradeoffs between properties such as consistency and availability, supporting local-first software and rich data models, and scaling live updates to full DevOps in software organizations. The Meerkat research program will enable a new era of developing apps that are more responsive, reliable, and evolvable than ever before.

Gradual verification, which supports explicitly partial specifications and verifies them with a combination of static and dynamic checks, makes verification more incremental and provides earlier feedback to developers. While an abstract, weakest precondition-based approach to gradual verification was previously proven sound, the approach did not provide sufficient guidance for implementation and optimization of the required run-time checks. More recently, gradual verification was implemented using symbolic execution techniques, but the soundness of the approach (as with related static checkers based on implicit dynamic frames) was an open question. This paper puts practical gradual verification on a sound footing with a formalization of symbolic execution, optimized run-time check generation, and run time execution. We prove our approach is sound; our proof also covers a core subset of the Viper tool, for which we are aware of no previous soundness result. Our formalization enabled us to find a soundness bug in an implemented gradual verification tool and describe the fix necessary to make it sound.

Current static verification techniques such as separation logic support a wide range of programs. However, such techniques only support complete and detailed specifications, which places an undue burden on users. To solve this problem, prior work proposed gradual verification, which handles complete, partial, or missing specifications by soundly combining static and dynamic checking. Gradual verification has also been extended to programs that manipulate recursive, mutable data structures on the heap. Unfortunately, this extension does not reward users with decreased dynamic checking as more specifications are written and more static guarantees are made. In fact, all properties are checked dynamically regardless of any static guarantees. Additionally, no full-fledged implementation of gradual verification exists so far, which prevents studying its performance and applicability in practice. We present Gradual C0, the first practicable gradual verifier for recursive heap data structures, which targets C0, a safe subset of C designed for education. Static verifiers supporting separation logic or implicit dynamic frames use symbolic execution for reasoning; so Gradual C0, which extends one such verifier, adopts symbolic execution at its core instead of the weakest liberal precondition approach used in prior work. Our approach addresses technical challenges related to symbolic execution with imprecise specifications, heap ownership, and branching in both program statements and specification formulas. We also deal with challenges related to minimizing insertion of dynamic checks and extensibility to other programming languages beyond C0. Finally, we provide the first empirical performance evaluation of a gradual verifier, and found that on average, Gradual C0 decreases run-time overhead between 7.1 and 40.2% compared to the fully dynamic approach used in prior work (for context, the worst cases for the approach by Wise et al. [ 2020 ] range from 0.1 to 4.5 seconds depending on the benchmark). Further, the worst-case scenarios for performance are predictable and avoidable. This work paves the way towards evaluating gradual verification at scale.

Program synthesis has the potential to democratize programming by enabling non-programmers to write software. But conventional approaches to synthesis may fail if given insufficient information - a common occurrence when asking non-experts to describe the application they want to write. This paper introduces a new concept-based program synthesis mechanism that can cope with incomplete knowledge, targeting low-code model-driven languages. Concepts are modelled in an ontology that represents user intent including basic actions (e.g. show, filter, and create) along with their associated data as well as basic user interface structures like screens or pages. Our synthesis framework consists of a system of derivation rules that supports deferred premises, which need not be immediately satisfied during synthesis. A derivation in which some deferred premises are missing will thus contain holes; semantically, it represents a proof that is conditional on the developer filling the holes with additional facts from the ontology. We translate derivations with holes to standard first-order logic derivations, where the holes are transformed into assumptions. We illustrate the feasibility and effectiveness of our framework with a proof-of-concept implementation and a set of illustrative examples.

Many Cyber-Physical Systems (CPS) have timing constraints that must be met by the cyber components (software and the network) to ensure safety. It is a tedious job to check if a CPS meets its timing requirement especially when it is distributed and the software and/or the underlying computing platforms are complex. Furthermore, the system design is brittle since a timing failure can still happen (e.g., network failure, soft error bit flip). In this article, we propose a new design methodology calledPlan Bwhere timing constraints of the CPS are monitored at runtime, and a proper backup routine is executed when a timing failure happens to ensure safety. We provide a model on how to express the desired timing behavior using a set of timing constructs in a C/C++ code and how to efficiently monitor them at the runtime. We showcase the effectiveness of our approach by conducting experiments on three case studies: (1) the full software stack for autonomous driving (Apollo), (2) a multi-agent system with 1/10th-scale model robots, and (3) a quadrotor for search and rescue application. We show that the system remains safe and stable even when intentional faults are injected to cause a timing failure. We also demonstrate that the system can achieve graceful degradation when a less extreme timing failure happens.

Effect systems have been a subject of active research for nearly four decades, with the most notable practical example being checked exceptions in programming languages such as Java. While many exception systems support abstraction, aggregation, and hierarchy (e.g., via class declaration and subclassing mechanisms), it is rare to see such expressive power in more generic effect systems. We designed an effect system around the idea of protecting system resources and incorporated our effect system into the Wyvern programming language. Similar to type members, a Wyvern object can have effect members that can abstract lower-level effects, allow for aggregation, and have both lower and upper bounds, providing for a granular effect hierarchy. We argue that Wyvern’s effects capture the right balance of expressiveness and power from the programming language design perspective. We present a full formalization of our effect-system design, showing that it allows reasoning about authority and attenuation. Our approach is evaluated through a security-related case study.

Static analysis tools typically address the problem of excessive false positives by requiring programmers to explicitly annotate their code. However, when faced with incomplete annotations, many analysis tools are either too conservative, yielding false positives, or too optimistic, resulting in unsound analysis results. In order to flexibly and soundly deal with partially-annotated programs, we propose to build upon and adapt the gradual typing approach to abstract-interpretation-based program analyses. Specifically, we focus on null-pointer analysis and demonstrate that a gradual null-pointer analysis hits a sweet spot, by gracefully applying static analysis where possible and relying on dynamic checks where necessary for soundness. In addition to formalizing a gradual null-pointer analysis for a core imperative language, we build a prototype using the Infer static analysis framework, and present preliminary evidence that the gradual null-pointer analysis reduces false positives compared to two existing null-pointer checkers for Infer. Further, we discuss ways in which the gradualization approach used to derive the gradual analysis from its static counterpart can be extended to support more domains. This work thus provides a basis for future analysis tools that can smoothly navigate the tradeoff between human effort and run-time overhead to reduce the number of reported false positives.

Programming language design research has traditionally focused primarily on theoretical properties and performance considerations. But programming languages are interfaces that programmers use to write programs. Recent work has begun to explore how to integrate interdisciplinary methods, including qualitative and quantitative user studies, into the language design process. I’ll describe how we applied such methods in two different designs, Obsidian and Glacier, some of the insights we gained, and discuss the larger impact these emerging methods can have on the field.

Programming language design requires making many usability-related design decisions. However, existing HCI methods can be impractical to apply to programming languages: languages have high iteration costs, programmers require significant learning time, and user performance has high variance. To address these problems, we adapted both formative and summative HCI methods to make them more suitable for programming language design. We integrated these methods into a new process, PLIERS, for designing programming languages in a user-centered way. We assessed PLIERS by using it to design two new programming languages. Glacier extends Java to enable programmers to express immutability properties effectively and easily. Obsidian is a language for blockchains that includes verification of critical safety properties. Empirical studies showed that the PLIERS process resulted in languages that could be used effectively by many programmers and revealed additional opportunities for language improvement.

Some blockchain programs (smart contracts) have included serious security vulnerabilities. Obsidian is a new typestate-oriented programming language that uses a strong type system to rule out some of these vulnerabilities. Although Obsidian was designed to promote usability to make it as easy as possible to write programs, strong type systems can cause a language to be difficult to use. In particular, ownership, typestate, and assets, which Obsidian uses to provide safety guarantees, have not seen broad adoption together in popular languages and result in significant usability challenges. We performed an empirical study with 20 participants comparing Obsidian to Solidity, which is the language most commonly used for writing smart contracts today. We observed that Obsidian participants were able to successfully complete more of the programming tasks than the Solidity participants. We also found that the Solidity participants commonly inserted asset-related bugs, which Obsidian detects at compile time.

Path dependent types have long served as an expressive component of the Scala programming language. They allow for the modelling of both bounded polymorphism and a degree of nominal subtyping. Nominality in turn provides the ability to capture first class modules. Thus a single language feature gives rise to a rich array of expressiveness. Recent work has proven path dependent types sound in the presence of both intersection and recursive types, but unfortunately typing remains undecidable, posing problems for programmers who rely on the results of type checkers. The Wyvern programming language is an object oriented language with path dependent types, recursive types and first class modules. In this paper we define two variants of Wyvern that feature decidable typing, along with machine checked proofs of decidability. Despite the restrictions, our approaches retain the ability to encode the parameteric polymorphism of Java generics along with many idioms of the Scala module system.

Current static verification techniques do not provide good support for incrementality, making it difficult for developers to focus on specifying and verifying the properties and components that are most important. Dynamic verification approaches support incrementality, but cannot provide static guarantees. To bridge this gap, prior work proposed gradual verification, which supports incrementality by allowing every assertion to be complete, partial, or omitted, and provides sound verification that smoothly scales from dynamic to static checking. The prior approach to gradual verification, however, was limited to programs without recursive data structures. This paper extends gradual verification to programs that manipulate recursive, mutable data structures on the heap. We address several technical challenges, such as semantically connecting iso- and equi-recursive interpretations of abstract predicates, and supporting gradual verification of heap ownership. This work thus lays the foundation for future tools that work on realistic programs and support verification within an engineering process in which cost-benefit trade-offs can be made.

We introduce a system called Penrose for creating mathematical diagrams. Its basic functionality is to translate abstract statements written in familiar math-like notation into one or more possible visual representations. Rather than rely on a fixed library of visualization tools, the visual representation is user-defined in a constraint-based specification language; diagrams are then generated automatically via constrained numerical optimization. The system is user-extensible to many domains of mathematics, and is fast enough for iterative design exploration. In contrast to tools that specify diagrams via direct manipulation or low-level graphics programming, Penrose enables rapid creation and exploration of diagrams that faithfully preserve the underlying mathematical meaning. We demonstrate the effectiveness and generality of the system by showing how it can be used to illustrate a diverse set of concepts from mathematics and computer graphics.

Blockchain platforms are coming into use for processing critical transactions among participants who have not established mutual trust. Many blockchains are programmable, supporting smart contracts , which maintain persistent state and support transactions that transform the state. Unfortunately, bugs in many smart contracts have been exploited by hackers. Obsidian is a novel programming language with a type system that enables static detection of bugs that are common in smart contracts today. Obsidian is based on a core calculus, Silica, for which we proved type soundness. Obsidian uses typestate to detect improper state manipulation and uses linear types to detect abuse of assets. We integrated a permissions system that encodes a notion of ownership to allow for safe, flexible aliasing. We describe two case studies that evaluate Obsidian’s applicability to the domains of parametric insurance and supply chain management, finding that Obsidian’s type system facilitates reasoning about high-level states and ownership of resources. We compared our Obsidian implementation to a Solidity implementation, observing that the Solidity implementation requires much boilerplate checking and tracking of state, whereas Obsidian does this work statically.

General-purpose programming languages typically define literal notation for only a small number of common data structures, like lists. This is unsatisfying because there are many other data structures for which literal notation might be useful, e.g. finite maps, regular expressions, HTML elements, SQL queries, syntax trees for various languages and chemical structures. There may also be different implementations of each of these data structures behind a common interface that could all benefit from common literal notation. This paper introducestyped literal macros (TLMs), which allow library providers to define new literal notation of nearly arbitrary design at any specified type or parameterized family of types. Compared to existing approaches, TLMs are uniquelyreasonable. TLM clients can reason abstractly, i.e. without examining grammars or generated expansions, about types and binding. The system only needs to convey to clients, via secondary notation, the inferredsegmentationof each literal body, which gives the locations and types of spliced subterms. TLM providers can reason modularly about syntactic ambiguity and expansion correctness according to clear criteria. This paper incorporates TLMs into Reason, an emerging alternative front-end for OCaml, and demonstrates, through several non-trivial case studies, how TLMs integrate with the advanced features of OCaml, including pattern matching and the module system. We also discuss optional integration with MetaOCaml, which allows TLM providers to be more confident about type correctness. Finally, we establish these abstract reasoning principles formally with a detailed type-theoretic account of expression and pattern TLMs for “core ML”.

The principle of least authority states that each component of the system should be given authority to access only the information and resources that it needs for its operation. This principle is fundamental to the secure design of software systems, as it helps to limit an application's attack surface and to isolate vulnerabilities and faults. Unfortunately, current programming languages do not provide adequate help in controlling the authority of application modules, an issue that is particularly acute in the case of untrusted third-party extensions. In this paper, we present a language design that facilitates controlling the authority granted to each application module. The key technical novelty of our approach is that modules are first-class, statically typed capabilities. First-class modules are essentially objects, and so we formalize our module system by translation into an object calculus and prove that the core calculus is type-safe and authority-safe. Unlike prior formalizations, our work defines authority non-transitively, allowing engineers to reason about software designs that use wrappers to provide an attenuated version of a more powerful capability. Our approach allows developers to determine a module's authority by examining the capabilities passed as module arguments when the module is created, or delegated to the module later during execution. The type system facilitates this by identifying which objects provide capabilities to sensitive resources, and by enabling security architects to examine the capabilities passed into and out of a module based only on the module's interface, without needing to examine the module's implementation code. An implementation of the module system and illustrative examples in the Wyvern programming language suggest that our approach can be a practical way to control module authority.

Though immutability has been long-proposed as a way to prevent bugs in software, little is known about how to make immutability support in programming languages effective for software engineers. We designed a new formalism that extends Java to support transitive class immutability, the form of immutability for which there is the strongest empirical support, and implemented that formalism in a tool called Glacier. We applied Glacier successfully to two real-world systems. We also compared Glacier to Java's final in a user study of twenty participants. We found that even after being given instructions on how to express immutability with final, participants who used final were unable to express immutability correctly, whereas almost all participants who used Glacier succeeded. We also asked participants to make specific changes to immutable classes and found that participants who used final all incorrectly mutated immutable state, whereas almost all of the participants who used Glacier succeeded. Glacier represents a promising approach to enforcing immutability in Java and provides a model for enforcement in other languages.

Structure editors allow programmers to edit the tree structure of a program directly. This can have cognitive benefits, particularly for novice and end-user programmers. It also simplifies matters for tool designers, because they do not need to contend with malformed program text.

The undisciplined use of shared mutable state can be a source of program errors when aliases unsafely interfere with each other. While protocol-based techniques to reason about interference abound, they do not address two practical concerns: the decidability of protocol composition and its integration with protocol abstraction. We show that our composition procedure is decidable and that it ensures safe interference even when composing abstract protocols. To evaluate the expressiveness of our protocol framework for safe shared memory interference, we show how this same protocol framework can be used to model safe, typeful message-passing concurrency idioms.

Context: Critical software systems developed for the government continue to be of lower quality than expected, despite extensive literature describing best practices in software engineering. Goal: We wanted to better understand the extent of certain issues in the field and the relationship to software quality. Method: We surveyed fifty software development professionals and asked about practices and barriers in the field and the resulting software quality. Results: There is evidence of certain problematic issues for developers and specific quality characteristics that seem to be affected. Conclusions: This motivates future work to address the most problematic barriers and issues impacting software quality.

This paper introduces typy, a statically typed programming language embedded by reflection into Python. typy features a fragmentary semantics, i.e. it delegates semantic control over each term, drawn from Python's fixed concrete and abstract syntax, to some contextually relevant user-defined semantic fragment. The delegated fragment programmatically 1) typechecks the term (following a bidirectional protocol); and 2) assigns dynamic meaning to the term by computing a translation to Python.

Programming languages can restrict state change by preventing it entirely (immutability) or by restricting which clients may modify state (read-only restrictions). The benefits of immutability and read-only restrictions in software structures have been long-argued by practicing software engineers, researchers, and programming language designers. However, there are many proposals for language mechanisms for restricting state change, with a remarkable diversity of techniques and goals, and there is little empirical data regarding what practicing software engineers want in their tools and what would benefit them. We systematized the large collection of techniques used by programming languages to help programmers prevent undesired changes in state. We interviewed expert software engineers to discover their expectations and requirements, and found that important requirements, such as expressing immutability constraints, were not reflected in features available in the languages participants used. The interview results informed our design of a new language extension for specifying immutability in Java. Through an iterative, participatory design process, we created a tool that reflects requirements from both our interviews and the research literature.

The Android platform is designed to support mutually untrusted third-party apps, which run as isolated processes but may interact via platform-controlled mechanisms, called Intents. Interactions among third-party apps are intended and can contribute to a rich user experience, for example, the ability to share pictures from one app with another. The Android platform presents an interesting point in a design space of module systems that is biased toward isolation, extensibility, and untrusted contributions. The Intent mechanism essentially provides message channels among modules, in which the set of message types is extensible. However, the module system has design limitations including the lack of consistent mechanisms to document message types, very limited checking that a message conforms to its specifications, the inability to explicitly declare dependencies on other modules, and the lack of checks for backward compatibility as message types evolve over time. In order to understand the degree to which these design limitations result in real issues, we studied a broad corpus of apps and cross-validated our results against app documentation and Android support forums. Our findings suggest that design limitations do indeed cause development problems. Based on our results, we outline further research questions and propose possible mitigation strategies.

Foundational models of object-oriented constructs typically model objects as records with a structural type. However, many object-oriented languages are class-based; statically-typed formal models of these languages tend to sacrifice the foundational nature of the record-based models, and in addition cannot express dynamic class loading or creation. In this paper, we explore how to model statically-typed object-oriented languages that support dynamic class creation using foundational constructs of type theory. We start with an extensible tag construct motivated by type theory, and adapt it to support static reasoning about class hierarchy and the tags supported by each object. The result is a model that better explains the relationship between object-oriented and functional programming paradigms, suggests a useful enhancement to functional programming languages, and paves the way for more expressive statically typed object-oriented languages. In that vein, we describe the design and implementation of the Wyvern language, which leverages our theory.

Application Programming Interfaces (APIs) often define protocols -- restrictions on the order of client calls to API methods. API protocols are common and difficult to use, which has generated tremendous research effort in alternative specification, implementation, and verification techniques. However, little is understood about the barriers programmers face when using these APIs, and therefore the research effort may be misdirected. To understand these barriers better, we perform a two-part qualitative study. First, we study developer forums to identify problems that developers have with protocols. Second, we perform a think-aloud observational study, in which we systematically observe professional programmers struggle with these same problems to get more detail on the nature of their struggles and how they use available resources. In our observations, programmer time was spent primarily on four types of searches of the protocol state space. These observations suggest protocol-targeted tools, languages, and verification techniques will be most effective if they enable programmers to efficiently perform state search.

The advent of multi-core systems set off a race to get concurrent programming to the masses. One of the challenging aspects of this type of system is how to deal with exceptional situations, since it is very difficult to assert the precise state of a concurrent program when an exception arises. In this paper we propose an exception-handling model for concurrent systems. Its main quality attributes are simplicity and expressiveness, allowing programmers to deal with exceptional situations in a concurrent setting in a familiar way. The proposal is centered on a new kind of exception type that defines new paths for exception propagation among concurrent threads of execution. In our model, beyond being able to control where exceptions are raised, the developer can define in which thread, and when during its execution, a particular exception will be handled. The proposed model has been implemented in Scala, and we show its application to the construction of concurrent software.

Cilk Plus and OpenMP are parallel language extensions for the C and C++ programming languages. The CPLEX Study Group of the ISO/IEC C Standards Committee is developing a proposal for a parallel programming extension to C that combines ideas from Cilk Plus and OpenMP. We conducted a preliminary comparison of Cilk Plus and OpenMP in a master's level course on security to evaluate the design tradeoffs in the usability and security of these two approaches. The eventual goal is to inform decision-making within the committee. We found several usability problems worthy of further investigation based on student performance, including declaring and using reductions, multi-line compiler directives, and the understanda-bility of task assignment to threads.

The aim of ÆMINIUM is to study the implications of having a concurrent-by-default programming language. This includes language design, runtime system, performance and software engineering considerations.

Typestate reflects how the legal operations on imperative objects can change at runtime as their internal state changes. A typestate checker can statically ensure, for instance, that an object method is only called when the object is in a state for which the operation is well defined. Prior work has shown how modular typestate checking can be achieved thanks to access permissions and state guarantees. However, typestate was not treated as a primitive language concept: typestate checkers are an additional verification layer on top of an existing language. In contrast, a typestate-oriented programming (TSOP) language directly supports expressing typestates. For example, in the Plaid programming language, the typestate of an object directly corresponds to its class, and that class can change dynamically. Plaid objects have not only typestate-dependent interfaces but also typestate-dependent behaviors and runtime representations. This article lays foundations for TSOP by formalizing a nominal object-oriented language with mutable state that integrates typestate change and typestate checking as primitive concepts. We first describe a statically typed language—Featherweight Typestate (FT)—where the types of object references are augmented with access permissions and state guarantees. We describe a novel flow-sensitive permission-based type system for FT. Because static typestate checking is still too rigid for some applications, we then extend this language into a gradually typed language—Gradual Featherweight Typestate (GFT). This language extends the notion of gradual typing to account for typestate: gradual typestate checking seamlessly combines static and dynamic checking by automatically inserting runtime checks into programs. The gradual type system of GFT allows programmers to write dynamically safe code even when the static type checker can only partly verify it.

Writing concurrent applications is extremely challenging, not only in terms of producing bug-free and maintainable software, but also for enabling developer productivity. In this article we present the Æminium concurrent-by-default programming language. Using Æminium programmers express data dependencies rather than control flow between instructions. Dependencies are expressed using permissions, which are used by the type system to automatically parallelize the application. The Æminium approach provides a modular and composable mechanism for writing concurrent applications, preventing data races in a provable way. This allows programmers to shift their attention from low-level, error-prone reasoning about thread interleaving and synchronization to focus on the core functionality of their applications. We study the semantics of Æminium through μ Æminium, a sound core calculus that leverages permission flow to enable concurrent-by-default execution. After discussing our prototype implementation we present several case studies of our system. Our case studies show up to 6.5X speedup on an eight-core machine when leveraging data group permissions to manage access to shared state, and more than 70% higher throughput in a Web server application.

While modularity is highly regarded as an important quality of software, it poses an educational dilemma: the true value of modularity is realized only as software evolves, but student homework, assignments and labs, once completed, seldom evolve. In addition, students seldom receive feedback regarding the modularity and evolvability of their designs. Prior work has shown that it is extremely easy for students and junior developers to introduce extra dependencies in their programs. In this paper, we report on a first experiment applying a tool-supported architecture review process in a software design class. To scientifically address this education problem, our first objective is to advance our understanding of why students make these modularity mistakes, and how the mistakes can be corrected. We propose tool-guided architecture review so that modularity problems in students' implementation can be revealed and their consequences can be assessed against possible change scenarios. Our pilot study shows that even students who understand the importance of modularity and have excellent programming skills may introduce additional harmful dependencies in their implementations. Furthermore, it is hard for them to detect the existence of these dependencies on their own. Our pilot study also showed that students need more formal training in architectural review to effectively detect and analyze these problems.

Programmers using an API often must follow protocols that specify when it is legal to call particular methods. Several techniques have been proposed to find violations of such protocols based on mined specifications. However, existing techniques either focus on single-object protocols or on particular kinds of bugs, such as missing method calls. There is no practical technique to find multi-object protocol bugs without a priori known specifications. In this paper, we combine a dynamic analysis that infers multi-object protocols and a static checker of API usage constraints into a fully automatic protocol conformance checker. The combined system statically detects illegal uses of an API without human-written specifications. Our approach finds 41 bugs and code smells in mature, real-world Java programs with a true positive rate of 51%. Furthermore, we show that the analysis reveals bugs not found by state of the art approaches.

In object-oriented programming, unique permissions to object references are useful for checking correctness properties such as consistency of typestate and noninterference of concurrency. To be usable, unique permissions must be borrowed --- for example, one must be able to read a unique reference out of a field, use it for something, and put it back. While one can null out the field and later reassign it, this paradigm is ungainly and requires unnecessary writes, potentially hurting cache performance. Therefore, in practice borrowing must occur in the type system, without requiring memory updates. Previous systems support borrowing with external alias analysis and/or explicit programmer management of fractional permissions. While these approaches are powerful, they are also awkward and difficult for programmers to understand. We present an integrated language and type system with unique, immutable, and shared permissions, together with new local permissions that say that a reference may not be stored to the heap. Our system also includes change permissions such as unique>>unique and unique>>none that describe how permissions flow in and out of method formal parameters. Together, these features support common patterns of borrowing, including borrowing multiple local permissions from a unique reference and recovering the unique reference when the local permissions go out of scope, without any explicit management of fractions in the source language. All accounting of fractional permissions is done by the type system "under the hood." We present the syntax and static and dynamic semantics of a formal core language and state soundness results. We also illustrate the utility and practicality of our design by using it to express several realistic examples.

Linear permissions have been proposed as a lightweight way to specify how an object may be aliased, and whether those aliases allow mutation. Prior work has demonstrated the value of permissions for addressing many software engineering concerns, including information hiding, protocol checking, concurrency, security, and memory management.

Objects model the world, and state is fundamental to a faithful modeling. Engineers use state machines to understand and reason about state transitions, but programming languages provide little support for building software based on state abstractions. We propose Plaid, a language in which objects are modeled not just in terms of classes, but in terms of changing abstract states. Each state may have its own representation, as well as methods that may transition the object into a new state. A formal model precisely defines the semantics of core Plaid constructs such as state transition and trait-like state composition. We evaluate Plaid through a series of examples taken from the Plaid compiler and the standard libraries of Smalltalk and Java. These examples show how Plaid can more closely model state-based designs, enhancing understandability, enhancing dynamic error checking, and providing reuse benefits.

Tracking the state of an object (in the sense of how a File can be in an Open or Closed state) is difficult not just because of the problem of managing state transitions but also due to the complexity introduced by aliasing. Unchecked duplication of object references makes local reasoning impossible by allowing situations where transitions can be triggered unexpectedly (for instance, passing aliased parameters to a method that expects unaliased parameters, or calling a method that has a side effect through an alias deeply nested in a data structure).

Engineers in many disciplines use state machines to reason about system changes, and many object-oriented libraries require their clients to follow state machine protocols. No existing language, however, has native support for state machines, and programmers often lose productivity and introduce errors when trying to understand and follow interaction protocols. The Plaid language extends the object paradigm with explicit states and state transitions, in order to better model object state transitions. In this paper, we present P laidcore, a core calculus for Plaid, which uses states and permissions to statically guarantee that clients use object protocols correctly.

An object diagram makes explicit the object structures that are only implicit in a class diagram. An object diagram may be missing and must extracted from the code. Alternatively, an existing diagram may be inconsistent with the code, and must be analyzed for conformance with the implementation. One can generalize the global object diagram of a system into a runtime architecture which abstracts objects into components, represents how those components interact, and can decompose a component into a nested sub-architecture.

Multiple inheritance has long been plagued with the "diamond" inheritance problem, leading to solutions that restrict expressiveness, such as mixins and traits. Instead, we address the diamond problem directly, considering two difficulties it causes: ensuring a correct semantics for object initializers, and typechecking multiple dispatch in a modular fashion-the latter problem arising even with multiple interface inheritance. We show that previous solutions to these problems are either unsatisfactory or cumbersome, and suggest a novel approach: supporting multiple inheritance but forbidding diamond inheritance. Expressiveness is retained through two features: a "requires" construct that provides a form of subtyping without inheritance (inspired by Scala), and a dynamically-dispatched "super" call similar to that found in traits. Through examples, we illustrate that inheritance diamonds can be eliminated via a combination of "requires" and ordinary inheritance. We provide a sound formal model for our language and demonstrate its modularity and expressiveness.

When a system fails to meet its specification, it can be difficult to find the source of the error and determine how to fix it. In this paper, we introduce error reporting logic (ERL), an algorithm and tool that produces succinct explanations for why a target system violates a specification expressed in first order predicate logic. ERL analyzes the specification to determine which parts contributed to the failure, and it displays an error message specific to those parts. Additionally, ERL uses a heuristic to determine which object in the target system is responsible for the error. Results from a small user study suggest that the combination of a more focused error message and a responsible object for the error helps users to find the failure in the system more effectively. The study also yielded insights into how the users find and fix errors that may guide future research.

The atomic block, a synchronization primitive provided to programmers in transactional memory systems, has the potential to greatly ease the development of concurrent software. However, atomic blocks can still be used incorrectly, and race conditions can still occur at the level of application logic. In this paper, we present a intraprocedural static analysis, formalized as a type system and proven sound, that helps programmers use atomic blocks correctly. Using access permissions, which describe how objects are aliased and modified, our system statically prevents race conditions and enforces typestate properties in concurrent programs. We have implemented a prototype static analysis for the Java language based on our system and have used it to verify several realistic examples.

We recently developed a static analysis to extract runtime architectures from object-oriented programs written in existing languages. The approach relies on adding ownership domain annotations to the code, and statically extracts a hierarchical runtime architecture from an annotated program.

The right software architecture is critical to achieving essential quality attributes, but these qualities are only realized if the program as implemented conforms to its intended architecture. Previous techniques for enforcing architecture are either unsound or place significant limitations on either architectural design or on implementation techniques. This paper presents the first system to statically enforce complete structural conformance between a rich, dynamic architectural description and object-oriented implementation code. We extend previous work to (1) explain what full structural conformance means in an object-oriented setting, and (2) enforce architectural structure in the presence of shared data. We show that the resulting system can express and enforce important structural constraints of an architecture, while still supporting key object-oriented implementation techniques. As a result of our conformance property, developers can be assured that their intended architecture is realized in code, so the system will exhibit the desired quality attributes.

Ownership domain annotations enable obtaining at compile-time the system's execution structure from the annotated program. The execution structure is sound, hierarchical (and thus more scalable) and conveys more design intent than flat object graphs obtained by existing static analyses that do not rely on annotations.

Objects often define usage protocols that clients must follow inorder for these objects to work properly. Aliasing makes itnotoriously difficult to check whether clients and implementations are compliant with such protocols. Accordingly, existing approaches either operate globally or severely restrict aliasing.

SAVCBS is a workshop for research and experience reports on the specification and verification of component-based systems.

Existing approaches to differencing and merging architectural views are based on restrictive assumptions such as requiring view elements to have unique identifiers or exactly matching types. We propose an approach based on structural information by generalizing a published polynomial-time tree-to-tree correction algorithm (that detects inserts, renames and deletes) into a novel algorithm to additionally detect restricted moves and support forcing and preventing matches between view elements. We incorporate the algorithm into tools to compare and merge component-and-connector (C&C) architectural views. Finally, we provide an empirical evaluation of the algorithm on case studies to find and reconcile interesting divergences between architectural views

One of the challenging problems for software developers is guaranteeing that a system as built is consistent with its architectural design. In this paper, we describe a technique that uses runtime observations about an executing system to construct an architectural view of the system. In this technique, we develop mappings that exploit regularities in system implementation and architectural style. These mappings describe how low-level system events can be interpreted as more abstract architectural operations and are formally defined using Colored Petri Nets. In this paper, we describe a system, called DiscoTect, that uses these mappings and we introduce the DiscoSTEP mapping language and its formal definition. Two case studies showing the application of DiscoTect suggest that the tool is practical to apply to legacy systems and can dynamically verify conformance to a preexisting architectural specification.

We demonstrate a tool to incrementally synchronize an Acme architectural model described in the Acme Architectural Description Language (ADL) with an implementation in ArchJava, an extension of the Java programming language that includes explicit architectural modeling constructs.

Today's module systems do not effectively support information hiding in the presence of shared mutable objects, causing serious problems in the development and evolution of large software systems. Ownership types have been proposed as a solution to this problem, but current systems have ad-hoc access restrictions and are limited to Java-like languages.In this paper, we describe System Fown, an extension of System F with references and ownership. Our design shows both how ownership fits into standard type theory and the encapsulation benefits it can provide in languages with first-class functions, abstract data types, and parametric polymorphism. By looking at ownership in the setting of SystemF, we were able to develop a design that is more principled and flexible than previous ownership type systems, while also providing stronger encapsulation guarantees.

Previous work has proven typestates to be useful for modeling protocols in object-oriented languages. We build on this work by addressing substitutability of subtypes as well as improving precision and conciseness of specifications. We propose a specification technique for objects based on abstract states that incorporates state refinement, method refinement, and orthogonal state dimensions. Union and intersection types form the underlying semantics of method specifications. The approach guarantees substitutability and behavioral subtyping. We designed a dynamic analysis to check existing object-oriented software for protocol conformance and validated our approach by specifying two standard Java libraries. We provide preliminary evidence for the usefulness of our approach.

In practice, there are many differences between an implementation-level architecture (such as one derived using architectural recovery techniques) and a more conceptual architecture used at design time. We present a lightweight, scalable, semi-automated, incremental approach for synchronizing a Componentand- Connector (C&C) view retrieved from an implementation with a conceptual C&C view described in an Architectural Description Language. Our approach can automatically detect corresponding elements in the presence of insertions, deletions, renames, and moves, and incrementally synchronize the two views.

One of the challenging problems for software developers is guaranteeing that a system as built is consistent with its architectural design. In this paper, we describe a technique that uses run time observations about an executing system to construct an architectural view of the system. With this technique, we develop mappings that exploit regularities in system implementation and architectural style. These mappings describe how low-level system events can be interpreted as more abstract architectural operations. We describe the current implementation of a tool that uses these mappings, and show that it can highlight inconsistencies between implementation and architecture.

Software architecture describes the structure of a system, enabling more effective design, program understanding, and formal analysis. However, existing approaches decouple implementation code from architecture, allowing inconsistencies, causing confusion, violating architectural properties, and inhibiting software evolution. ArchJava is an extension to Java that seamlessly unifies software architecture with implementation, ensuring that the implementation conforms to architectural constraints. A case study applying ArchJava to a circuit-design application suggests that ArchJava can express architectural structure effectively within an implementation, and that it can aid in program understanding and software evolution.

One of the primary challenges in building and evolving large object-oriented systems is understanding aliasing between objects. Unexpected aliasing can lead to broken invariants, mistaken assumptions, security holes, and surprising side effects, all of which may lead to software defects and complicate software evolution.This paper presents AliasJava, a capability-based alias annotation system for Java that makes alias patterns explicit in the source code, enabling developers to reason more effectively about the interactions in a complex system. We describe our implementation, prove the soundness of the annotation system, and give an algorithm for automatically inferring alias annotations. Our experience suggests that the annotation system is practical, that annotation inference is efficient and yields appropriate annotations, and that the annotations can express important invariants of data structures and of software architectures.