The BBC micro:bit is a pocket-sized, battery-powered device that introduces students to coding and computational thinking through the lens of physical computing. It can be incorporated in a variety of interactive projects and combined with a range of commercially available accessories. These include display shields that support richer user interaction with the micro:bit via a small colour screen and additional button inputs.

Symbolic automata are finite state automata that support potentially infinite alphabets, such as the set of rational numbers, generally applied to regular expressions and languages over finite words. In symbolic automata (or automata modulo 𝒜), an alphabet is represented by an effective Boolean algebra 𝒜, supported by a decision procedure for satisfiability. Regular languages over infinite words (so called ω -regular languages) have a rich history paralleling that of regular languages over finite words, with well known applications to model checking via Büchi automata and temporal logics. We generalize symbolic automata to support ω -regular languages via transition terms and symbolic derivatives , bringing together a variety of classic automata and logics in a unified framework that provides all the necessary ingredients to support symbolic model checking modulo 𝒜. In particular, we define: (1) alternating Büchi automata modulo 𝒜( AB W 𝒜 ) as well (non-alternating) nondeterministic Büchi automata modulo 𝒜( NB W 𝒜 );(2) an alternation elimination algorithm Æ that incrementally constructs an NB W 𝒜 from an AB W 𝒜 , and can also be used for constructing the product of two NB W 𝒜 ; (3) a definition of linear temporal logic modulo 𝒜, LTL ⟨𝒜⟩, that generalizes Vardi's construction of alternating Büchi automata from LTL, using (2) to go from LTL modulo 𝒜 to NB W 𝒜 via AB W 𝒜 . Finally, we present RLTL ⟨ 𝒜 ⟩, a combination of LTL ⟨ 𝒜 ⟩ with extended regular expressions modulo 𝒜 that generalizes the Property Specification Language (PSL). Our combination allows regex complement , that is not supported in PSL but can be supported naturally by using transition terms. We formalize the semantics of RLTL ⟨ 𝒜 ⟩ using the Lean proof assistant and formally establish correctness of the main derivation theorem.

This workshop will bring together researchers and educators to imagine a future of low-cost, widely-available digital making for children, both within the STEAM classroom and beyond. In particular, we are interested in expanding the reach of digital making with programmable microcontrollers (such as Arduino, the BBC micro:bit, etc.) to underrepresented children in the STEAM fields, which includes historically excluded or marginalized children as well as those lacking access to computers and/or the Internet. Participants will report on their experience helping children learn about digital technology while creating wearables, robotics, environmental sensors and more. Participants who submit a position paper or work-in-progress report will have an opportunity to present their work and ideas. From these presentations, we will select emerging themes to discuss.

Physical computing has emerged as an effective approach to introducing computing and coding to students. One of the most popular enabling tools is the BBC micro:bit, well-known for its positive impact on teaching programming and driving engagement in the classroom. We extend these benefits by developing a new approach to coding with micro:bit: MicroCode. Unlike other experiences, MicroCode couples the micro:bit with a low-cost handheld accessory to enable live and portable programming via an on-device visual programming language; no separate host computer is needed. We present the design of MicroCode and the findings of a study in which we interviewed five primary school teachers and 60 children aged 10-11 working with MicroCode. The outcomes of the study show that MicroCode raised children’s engagement and stimulated the development of a strong sense of agency on coding activities, while teachers felt empowered to adopt situated and cross-curricular learning approaches.

The traditional approach to programming embedded systems is monolithic: firmware on a microcontroller contains both application code and the drivers needed to communicate with sensors and actuators, using low-level protocols such as I2C, SPI, and RS232. In comparison, software development for the cloud has moved to a service-based development and operation paradigm: a service provides a discrete unit of functionality that can be accessed remotely by an application, or other service, but is independently managed and updated. We propose, design, implement, and evaluate a service-based approach to prototyping embedded systems called Jacdac. Jacdac defines a service specification language, designed especially for embedded systems, along with a host of specifications for a variety of sensors and actuators. With Jacdac, each sensor/actuator in a system is paired with a low-cost microcontroller that advertises the services that represent the functionality of the underlying hardware over an efficient and low-cost single-wire bus protocol. A separate microcontroller executes the user's application program, which is a client of the Jacdac services on the bus. Our evaluation shows that Jacdac supports a service-based abstraction for sensors/actuators at low cost and reasonable performance, with many benefits for prototyping: ease of use via the automated discovery of devices and their capabilities, substitution of same-service devices for each other, as well as high-level programming, monitoring, and debugging. We also report on the experience of bringing Jacdac to commercial availability via third-party manufacturers.

Prior work has broadly explored empowering children to learn to program by making video games. However, such work has rarely considered the role of families in this learning, leaving many open questions about how inter-generational collaborations might support and constrain learning. To investigate these opportunities, we conducted a family-based study of TileCode, a rule-based programming platform for video-game programming, and scaffolded a 4-week series of game programming activities with 19 children (9 to 14 years old) and 16 parents. Using a joint media engagement lens to analyze family knowledge and programming strategies, we found: 1) families demonstrated many dynamic collaboration patterns distinct from pair programming and other collaboration models, 2) parents played a unique role in scaffolding and guiding more complex designs and programming tasks, 3) families found it challenging to start their games from scratch but benefited greatly from having programming patterns for particular game behaviors. These findings suggest the need for game programming platforms to design around the unique kinds of collaboration in inter-generational domain-specific programming.

Technology has become increasingly pervasive in the creative and experimental environment of the avant-garde fashion runway, particularly in relation to its garments. However, several disciplines are often necessary when exploring technologies for the construction of expressive garments (e.g. garments that respond to their environment), creating a barrier for fashion designers that has limited their ability to leverage new technologies. To help overcome this barrier, we designed and deployed Brookdale, a prototyping system for wearable technology consisting of new plug-and-play hardware that can be programmed using drag-and-drop software. Brookdale was created using a 24-week participatory design process with 17 novice fashion-tech designers. At the end of the 24 week process, designers showcased their Brookdale-enhanced garment collections at an avant-garde fashion-tech runway show in New York City. We report on the experiences, outcomes, and lessons learned throughout this process, and describe results from interviews with the fashion-tech designers 16 weeks after the fashion show, demonstrating the lasting positive impact of Brookdale.

Low-cost microcontroller boards like the BBC micro:bit are used to engage and inspire students worldwide to learn more about computing. Easy-to-use web-based programming environments and low-cost hardware allow novices to build physical computing systems with the micro:bit – systems that sense and respond to the real world. However, devices such as the micro:bit may not capture the attention of every student, as the interests of some may lie in graphic design, animation, or other areas that are not the main focus of physical computing.

We present TileCode, a video game creation environment that runs on battery-powered microcontroller-based gaming handhelds. Our work is motivated by the popularity of retro video games, the availability of low-cost gaming handhelds loaded with many such games, and the concomitant lack of a means to create games on the same handhelds. With TileCode, we seek to close the gap between the consumers and creators of video games and to motivate more individuals to participate in the design and creation of their own games. The TileCode programming model is based on tile maps and provides a visual means for specifying the context around a sprite, how a sprite should move based on that context, and what should happen upon sprite collisions. We demonstrate that a variety of popular video games can be programmed with TileCode using 10-15 visual rules and compare/contrast with block-based versions of the same games implemented using MakeCode Arcade.

While the programming of microcontroller-based embeddable devices typically is the realm of the C language, such devices are now finding their way into the classroom for CS education, even at the level of middle school. As a result, the use of scripting languages (such as JavaScript and Python) for microcontrollers is on the rise.

Historically, embedded systems development has been a specialist skill, requiring knowledge of low-level programming languages, complex compilation toolchains, and specialist hardware, firmware, device drivers and applications. However, it has now become commonplace for a broader range of non-specialists to engage in the making (design and development) of embedded systems - including educators to motivate and excite their students in the classroom. This diversity brings its own set of unique requirements, and the complexities of existing embedded systems development platforms introduce insurmountable barriers to entry. In this paper we present the motivation, requirements, implementation, and evaluation of a new programming platform that enables novice users to create effective and efficient software for embedded systems. The platform has two major components: (1) Microsoft MakeCode (www.makecode.com), a web app that encapsulates an accessible IDE for microcontrollers; and (2) CODAL, an efficient component-oriented C++ runtime for microcontrollers. We show how MakeCode and CODAL combine to provide an accessible, cross-platform, installation-free, high level programming experience for embedded devices without sacrificing performance and efficiency.

Paper-based fabrication techniques offer powerful opportunities to prototype new technological interfaces. Typically, paper-based interfaces are either static mockups or require integration with sensors to provide real-time interactivity. The latter can be challenging and expensive, requiring knowledge of electronics, programming, and sensing. But what if computer vision could be combined with prototyping domain-aware programming tools to support the rapid construction of interactive, paper-based tangible interfaces? We designed a toolkit called ARcadia that allows for rapid, low-cost prototyping of TUIs that only requires access to a webcam, a web browser, and paper. ARcadia brings paper prototypes to life through the use of marker based augmented reality (AR). Users create mappings between real-world tangible objects and different UI elements. After a crafting and programming phase, all subsequent interactions take place with the tangible objects. We evaluated ARcadia in a workshop with 120 teenage girls and found that tangible AR technologies can empower novice technology designers to rapidly construct and iterate on their ideas.

Across the globe, it is now commonplace for educators to engage in the making (design and development) of embedded systems in the classroom to motivate and excite their students. This new domain brings its own set of unique requirements. Historically, embedded systems development requires knowledge of low-level programming languages, local installation of compilation toolchains, device drivers, and applications. For students and educators, these requirements can introduce insurmountable barriers.

The micro:bit (http://www.microbit.org) is a pocket-sized, programmable computing device, designed to engage people with computing technology. The micro:bit is visually appealing, fun, easy to code and inexpensive. It is widely available at schools in the United Kingdom and is now being rolled out world-wide. Key features of the micro:bit that make it a great device for physical computing include a display of 25 LEDs, two programmable input buttons, a USB connector, an edge connector, built-in sensors (e.g. accelerometer, compass and temperature sensor), Bluetooth and a battery pack connector. With these physical attributes, the micro:bit can be used to interact with the world in engaging ways such as a watch, a guitar or a moisture sensor. Multi-person games and apps are possible since micro:bits can communicate with each other. Programming the micro:bit can take place on almost any device (laptop, tablet, desktop) that has a modern browser and a USB connection. The micro:bit platform supports programming in a block-based language or a safe version of JavaScript, which provides a progression for learners of different ages and experience levels. This demo will appeal to computer education researchers specializing in K-12 as well as to instructors wanting a new way to introduce computing in CS101 with a "maker" flavor. In the demo we will show the platform and the hardware. Attendees will have the chance to create apps on real micro:bits. It will be helpful to bring a device with a browser.

Software-defined networking (SDN) is a new paradigm for operating and managing computer networks. SDN enables logically-centralized control over network devices through a "controller" software that operates independently from the network hardware, and can be viewed as the network operating system. Network operators can run both inhouse and third-party SDN programs (often called applications) on top of the controller, e.g., to specify routing and access control policies. SDN opens up the possibility of applying formal methods to prove the correctness of computer networks. Indeed, recently much effort has been invested in applying finite state model checking to check that SDN programs behave correctly. However, in general, scaling these methods to large networks is challenging and, moreover, they cannot guarantee the absence of errors.

Software tools researchers can accelerate their ability to learn by exposing tools to users via web technologies, allowing them to observe and test the interactions between humans and tools. At Microsoft Research, we have developed a web service (http://www.rise4fun.com/) for such a purpose that is available for community use.

We study the problem of suggesting code repairs at design time, based on the warnings issued by modular program verifiers. We introduce the concept of a verified repair, a change to a program's source that removes bad execution traces while increasing the number of good traces, where the bad/good traces form a partition of all the traces of a program. Repairs are property-specific. We demonstrate our framework in the context of warnings produced by the modular cccheck (a.k.a. Clousot) abstract interpreter, and generate repairs for missing contracts, incorrect locals and objects initialization, wrong conditionals, buffer overruns, arithmetic overflow and incorrect floating point comparisons. We report our experience with automatically generating repairs for the .NET framework libraries, generating verified repairs for over 80% of the warnings generated by cccheck.

Modern programming frameworks provide enormous libraries arranged in complex structures, so much so that a large part of modern programming is searching for APIs that surely exist" somewhere in an unfamiliar part of the framework. We present a novel way of phrasing a search for an unknown API: the programmer simply writes an expression leaving holes for the parts they do not know. We call these expressions partial expressions. We present an efficient algorithm that produces likely completions ordered by a ranking scheme based primarily on the similarity of the types of the APIs suggested to the types of the known expressions. This gives a powerful language for both API discovery and code completion with a small impedance mismatch from writing code. In an automated experiment on mature C# projects, we show our algorithm can place the intended expression in the top 10 choices over 80% of the time.

Software drivers are usually developed after hardware devices become available. This dependency can induce a long product cycle. Although co-simulation and co-verification techniques have been utilized to facilitate the driver development, Hardware/Software (HW/SW) interface models, as the test harnesses, are often challenging to specify. Such interface models should have formal semantics, be efficient for testing, and cover all HW/SW behaviors described by HW/SW interface protocols. We present an approach to formalizing HW/SW interface specifications, where we propose a semantic model, relative atomicity, to capture the concurrency model in HW/SW interfaces; demonstrate our approach via a realistic example; elaborate on how we have utilized this approach in device/driver development process; and discuss criteria for evaluating our formal specifications. We have detected fifteen issues in four English specifications. Furthermore, our formal specifications are readily useful as the test harnesses for co-verification, which has discovered twelve real bugs in five industrial driver programs.

Parallel or incremental versions of an algorithm can significantly outperform their counterparts, but are often difficult to develop. Programming models that provide appropriate abstractions to decompose data and tasks can simplify parallelization. We show in this work that the same abstractions can enable both parallel and incremental execution. We present a novel algorithm for parallel self-adjusting computation. This algorithm extends a deterministic parallel programming model (concurrent revisions) with support for recording and repeating computations. On record, we construct a dynamic dependence graph of the parallel computation. On repeat, we reexecute only parts whose dependencies have changed.

Multicore computers are now the norm. Taking advantage of these multiple cores entails parallel and concurrent programming. There is therefore a pressing need for courses that teach effective programming on multicore architectures. We believe that such courses should emphasize high-level abstractions for performance and correctness and be supported by tools. This paper presents a set of freely available course materials for parallel and concurrent programming, along with a testing tool for performance and correctness concerns called Alpaca (A Lovely Parallelism And Concurrency Analyzer). These course materials can be used for a comprehensive parallel and concurrent programming course, à la carte throughout an existing curriculum, or as starting points for graduate special topics courses. We also discuss tradeoffs we made in terms of what to include in course materials.

In the mid 1990s, I was (tangentially) part of an effort in Bell Labs called the "Code Decay" project. The hypothesis of this project was that over time code becomes fragile (more difficult to change without introducing problems), and that this process of decay could be empirically validated. This effort awakened me to the power of combining statistical expertise with software engineering expertise to address pressing problems of software production in a statistically valid manner. I will revisit some of the work we did in the Code Decay project at Bell Labs and then turn to what has been happening in this area in Microsoft in the last five years. In particular, I will trace how we have progressed from studying the data produced by product teams to validate hypotheses, to being actively involved with the product groups in creating and evaluating new tools and techniques for empirically-based software production.

We present a case study in which a team of test engineers at Microsoft applied a feedback-directed random testing tool to a critical component of the .NET architecture. Due to its complexity and high reliability requirements, the component had already been tested by 40 test engineers over five years, using manual testing and many automated testing techniques.

Commercial software development is a complex task that requires a thorough understanding of the architecture of the software system. We analyze the Windows Server 2003 operating system in order to assess the relationship between its software dependencies, churn measures and post-release failures. Our analysis indicates the ability of software dependencies and churn measures to be efficient predictors of post-release failures. Further, we investigate the relationship between the software dependencies and churn measures and their ability to assess failure-proneness probabilities at statistically significant levels.

We present a technique that improves random test generation by incorporating feedback obtained from executing test inputs as they are created. Our technique builds inputs incrementally by randomly selecting a method call to apply and finding arguments from among previously-constructed inputs. As soon as an input is built, it is executed and checked against a set of contracts and filters. The result of the execution determines whether the input is redundant, illegal, contract-violating, or useful for generating more inputs. The technique outputs a test suite consisting of unit tests for the classes under test. Passing tests can be used to ensure that code contracts are preserved across program changes; failing tests (that violate one or more contract) point to potential errors that should be corrected. Our experimental results indicate that feedback-directed random test generation can outperform systematic and undirected random test generation, in terms of coverage and error detection. On four small but nontrivial data structures (used previously in the literature), our technique achieves higher or equal block and predicate coverage than model checking (with and without abstraction) and undirected random generation. On 14 large, widely-used libraries (comprising 780KLOC), feedback-directed random test generation finds many previously-unknown errors, not found by either model checking or undirected random generation.

We present a new approach for performing predicate abstraction based on symbolic decision procedures. Intuitively, a symbolic decision procedure for a theory takes a set of predicates in the theory and symbolically executes a decision procedure on all the subsets over the set of predicates. The result of the symbolic decision procedure is a shared expression (represented by a directed acyclic graph) that implicitly represents the answer to a predicate abstraction query. We present symbolic decision procedures for the logic of Equality and Uninterpreted Functions (EUF) and Difference logic (DIFF) and show that these procedures run in pseudo-polynomial (rather than exponential) time. We then provide a method to construct symbolic decision procedures for simple mixed theories (including the two theories mentioned above) using an extension of the Nelson-Oppen combination method. We present preliminary evaluation of our Procedure on predicate abstraction benchmarks from device driver verification in SLAM.

Bugs in kernel-level device drivers cause 85% of the system crashes in the Windows XP operating system [44]. One of the sources of these errors is the complexity of the Windows driver API itself: programmers must master a complex set of rules about how to use the driver API in order to create drivers that are good clients of the kernel. We have built a static analysis engine that finds API usage errors in C programs. The Static Driver Verifier tool (SDV) uses this engine to find kernel API usage errors in a driver. SDV includes models of the OS and the environment of the device driver, and over sixty API usage rules. SDV is intended to be used by driver developers "out of the box." Thus, it has stringent requirements: (1) complete automation with no input from the user; (2) a low rate of false errors. We discuss the techniques used in SDV to meet these requirements, and empirical results from running SDV on over one hundred Windows device drivers.

What is it that makes software fail? In an empirical study of the post-release defect history of five Microsoft software systems, we found that failure-prone software entities are statistically correlated with code complexity measures. However, there is no single set of complexity metrics that could act as a universally best defect predictor. Using principal component analysis on the code metrics, we built regression models that accurately predict the likelihood of post-release defects for new entities. The approach can easily be generalized to arbitrary projects; in particular, predictors obtained from one project can also be significant for new, similar projects.

The use of assertions in software development is thought to help produce quality software. Unfortunately, there is scant empirical evidence in commercial software systems for this argument to date. This paper presents an empirical case study of two commercial software components at Microsoft Corporation. The developers of these components systematically employed assertions, which allowed us to investigate the relationship between software assertions and code quality. We also compare the efficacy of assertions against that of popular bug finding techniques like source code static analysis tools. We observe from our case study that with an increase in the assertion density in a file there is a statistically significant decrease in fault density. Further, the usage of software assertions in these components found a large percentage of the faults in the bug database

The benefits that a software organization obtains from estimates of product quality are dependent upon how early in the product cycle that these estimates are available. Early estimation of software quality can help organizations make informed decisions about corrective actions. To provide such early estimates we present an empirical case study of two large scale commercial operating systems, Windows XP and Windows Server 2003. In particular, we leverage various historical in-process and product metrics from Windows XP binaries to create statistical predictors to estimate the post-release failures/failure-proneness of Windows Server 2003 binaries. These models estimate the failures and failure-proneness of Windows Server 2003 binaries at statistically significant levels. Our study is unique in showing that historical predictors for a software product line can be useful, even at the very large scale of the Windows operating system

We present a method for static program analysis that leverages tests and concrete program executions. State abstractions generalize the set of program states obtained from concrete executions. A theorem prover then checks that the generalized set of concrete states covers all potential executions and satisfies additional safety properties. Our method finds the same potential errors as the mostprecise abstract interpreter for a given abstraction and is potentially more efficient. Additionally, it provides a new way to tune the performance of the analysis by alternating between concrete execution and theorem proving. We have implemented our technique in a prototype for checking properties of C# programs.

Abstraction is a key technique for reasoning about systems with very large or even infinite state spaces. When a system is composed of reactive components, the interaction between the components is modeled by a multi-player game and verification corresponds to finding winners in the game. We describe an abstraction-refinement framework for multi-player games, with respect to specifications in the alternating mu-calculus (AMC). Our framework is based on abstract alternating transition systems (AATSs). Each agent in an AATS has transitions that over-approximate its power and transitions that under-approximate its power. We define the framework, define a 3-valued semantics for AMC formulas in an AATS, study the model-checking problem, define an abstraction preorder between AATSs, suggest a refinement procedure (in case model checking returns an indefinite answer), and study the completeness of the framework. For the case of predicate abstraction, we show how reasoning can be automated with a theorem prover. Abstractions of multi-player games have been studied in the past. Our main contribution with respect to earlier work is that we study general (rather than only turn-based) ATSs, we add a refinement procedure on top of the model checking procedure, and our abstraction preorder is parameterized by a set of agents

Software systems evolve over time due to changes in requirements, optimization of code, fixes for security and reliability bugs etc. Code churn, which measures the changes made to a component over a period of time, quantifies the extent of this change. We present a technique for early prediction of system defect density using a set of relative code churn measures that relate the amount of churn to other variables such as component size and the temporal extent of churn.Using statistical regression models, we show that while absolute measures of code churn are poor predictors of defect density, our set of relative measures of code churn is highly predictive of defect density. A case study performed on Windows Server 2003 indicates the validity of the relative code churn measures as early indicators of system defect density. Furthermore, our code churn metric suite is able to discriminate between fault and not fault-prone binaries with an accuracy of 89.0 percent.

During software development it is helpful to obtain early estimates of the defect density of software components. Such estimates identify fault-prone areas of code requiring further testing. We present an empirical approach for the early prediction of pre-release defect density based on the defects found using static analysis tools. The defects identified by two different static analysis tools are used to fit and predict the actual pre-release defect density for Windows Server 2003. We show that there exists a strong positive correlation between the static analysis defect density and the pre-release defect density determined by testing. Further, the predicted pre-release defect density and the actual pre-release defect density are strongly correlated at a high degree of statistical significance. Discriminant analysis shows that the results of static analysis tools can be used to separate high and low quality components with an overall classification rate of 82.91%.

Predicate abstraction is a technique for creating abstract models of software that are amenable to model checking algorithms. We show how polymorphism, a well-known concept in programming languages and program analysis, can be incorporated in a predicate abstraction algorithm for C programs. The use of polymorphism in predicates, via the introduction of symbolic names for values, allows us to model the effect of a procedure independent of its calling contexts. Therefore, we can safely and precisely abstract a procedure once and then reuse this abstraction across multiple calls and multiple applications containing the procedure. Polymorphism also enables us to handle programs that need to be analyzed in an open environment, for all possible callers. We have proved that our algorithm is sound and have implemented it in the C2BP tool as part of the SLAM software model checking toolkit.

There is significant room for improving users' experiences with model checking tools. An error trace produced by a model checker can be lengthy and is indicative of a symptom of an error. As a result, users can spend considerable time examining an error trace in order to understand the cause of the error. Moreover, even state-of-the-art model checkers provide an experience akin to that provided by parsers before syntactic error recovery was invented: they report a single error trace per run. The user has to fix the error and run the model checker again to find more error traces.We present an algorithm that exploits the existence of correct traces in order to localize the error cause in an error trace, report a single error trace per error cause, and generate multiple error traces having independent causes. We have implemented this algorithm in the context of slam, a software model checker that automatically verifies temporal safety properties of C programs, and report on our experience using it to find and localize errors in device drivers. The algorithm typically narrows the location of a cause down to a few lines, even in traces consisting of hundreds of statements.

The goal of the SLAM project is to check whether or not a program obeys "API usage rules" that specify what it means to be a good client of an API. The SLAM toolkit statically analyzes a C program to determine whether or not it violates given usage rules. The toolkit has two unique aspects: it does not require the programmer to annotate the source program (invariants are inferred); it minimizes noise (false error messages) through a process known as "counterexample-driven refinement". SLAM exploits and extends results from program analysis, model checking and automated deduction. We have successfully applied the SLAM toolkit to Windows XP device drivers, to both validate behavior and find defects in their usage of kernel APIs.

Software tools can improve the quality and maintainability of software, but are expensive to acquire, deploy, and maintain, especially in large organizations. We explore how to quantify the effects of a software tool once it has been deployed in a development environment. We present an effort-analysis method that derives tool usage statistics and developer actions from a project's change history (version control system) and uses a novel effort estimation algorithm to quantify the effort savings attributable to tool usage. We apply this method to assess the impact of a software tool called VE, a version-sensitive editor used in Bell Labs. VE aids software developers in coping with the rampant use of certain preprocessor directives (similar to #if/#endif in C source files). Our analysis found that developers were approximately 40 percent more productive when using VE than when using standard text editors.

Flow-sensitive data analyses can lose precision because they assume that all paths in a control-flow graph are executable (feasible). Path-sensitive dataflow analyses can rule out infeasible paths by tracking correlations between dataflow facts. To track such correlations, in general, requires recording a set of sets of facts per statement in a program. Naive representation of such sets can lead to a very high memory consumption and running time.

Model checking has been widely successful in validating and debugging designs in the hardware and protocol domains. However, state-space explosion limits the applicability of model checking tools, so model checkers typically operate on abstractions of systems.

The maturity of object-oriented methods has led to the wide availability of container classes: classes that encapsulate classical data structures and algorithms. Container classes are included in the C++ and Java standard libraries, and in many proprietary libraries. The wide availability and use of these classes makes reliability important, and testing plays a central role in achieving that reliability. The large number of cases necessary for thorough testing of container classes makes automated testing essential. This paper presents a novel approach for automated testing of container classes based on combinatorial algorithms for state generation. The approach is illustrated with black-box and white-box test drivers for a class implemented with the red–black tree data structure, used widely in industry and, in particular, in the C++ Standard Template Library. The white-box driver is based on a new algorithm for red–black tree generation. The drivers are evaluated experimentally, providing quantitative measures of their effectiveness in terms of block and path coverage. The results clearly show that the approach is affordable in terms of development cost and execution time, and effective with respect to coverage achieved. The results also provide insight into the relative advantages of black-box and white-box drivers, and into the difficult problem of infeasible paths. Copyright © 2000 John Wiley & Sons, Ltd.

Article Free Access Share on Using version control data to evaluate the impact of software tools Authors: David Atkins Software Production Research Dept., Bell Laboratories, Lucent Technologies Software Production Research Dept., Bell Laboratories, Lucent TechnologiesView Profile , Thomas Ball Software Production Research Dept., Bell Laboratories, Lucent Technologies Software Production Research Dept., Bell Laboratories, Lucent TechnologiesView Profile , Todd Graves Software Production Research Dept., National Institute of Statistical Sciences, Bell Laboratories, Lucent Technologies Software Production Research Dept., National Institute of Statistical Sciences, Bell Laboratories, Lucent TechnologiesView Profile , Audris Mockus Software Production Research Dept., Bell Laboratories, Lucent Technologies Software Production Research Dept., Bell Laboratories, Lucent TechnologiesView Profile Authors Info & Claims ICSE '99: Proceedings of the 21st international conference on Software engineeringMay 1999 Pages 324–333https://doi.org/10.1145/302405.302649Published:16 May 1999Publication History 20citation815DownloadsMetricsTotal Citations20Total Downloads815Last 12 Months26Last 6 weeks6 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

A form-based service is one in which the flow of data between service and user is described by a sequence of query/response interactions, or forms. Mawl is a domain-specific language for programming form-based services in a device-independent manner. We focus on Mawl's form abstraction, which is the means for separating service logic from user interface description, and show how this simple abstraction addresses seven issues in service creation, analysis, and maintenance: compile-time guarantees, implementation flexibility, rapid prototyping, testing and validation, support for multiple devices, composition of services, and usage analysis.

Automated analyses for regression test selection (RTS) attempt to determine if a modified program, when run on a test t, will have the same behavior as an old version of the program run on t, but without running the new program on t. RTS analyses must confront a price/performance tradeoff: a more precise analysis might be able to eliminate more tests, but could take much longer to run.We focus on the application of control flow analysis and control flow coverage, relatively inexpensive analyses, to the RTS problem, considering how the precision of RTS algorithms can be affected by the type of coverage information collected. We define a strong optimality condition (edge-optimality) for RTS algorithms based on edge coverage that precisely captures when such an algorithm will report that re-testing is needed, when, in actuality, it is not. We reformulate Rothermel and Harrold's RTS algorithm and present three new algorithms that improve on it, culminating in an edge-optimal algorithm. Finally, we consider how path coverage can be used to improve the precision of RTS algorithms.

Edge profiles are the traditional control flow profile of choice for profile-directed compilation. They have been the basis of path-based optimizations that select paths, even though edge profiles contain strictly less information than path profiles. Recent work on path profiling has suggested that path profiles are superior to edge profiles in practice.We present theoretic and algorithmic results that may be used to determine when an edge profile is a good predictor of hot paths (and what those hot paths are) and when it is a poor predictor. Our algorithms efficiently compute sets of definitely and potentially hot paths in a graph annotated with an edge profile. A definitely hot path has a frequency greater than some non-zero lower bound in all path profiles that induce a given edge profile.Experiments on the SPEC95 benchmarks show that a huge percentage of the execution frequency in these programs is dominated by definitely hot paths (on average, 84% for FORTRAN benchmarks and 76% for C benchmarks). We also show that various hot path selection algorithms based on edge profiles work extremely well in most cases, but that path profiling is needed in some cases. These results indicate the usefulness of our algorithms for characterizing edge profiles and selecting hot paths.

Implementing, validating, modifying, or reengineering an object-oriented system requires an understanding of the object and class interactions which occur as a program executes.This work seeks to identify, visualize, and analyze interactions in object-oriented program executions as a means for examining and understanding dynamic behavior.We have discovered recurring interaction scenarios in program executions that can be used as abstractions in the understanding process, and have developed a means for identifying these interaction patterns.Our visualizations focus on supporting design recovery, validation, and reengineering tasks, and can be applied to both object-oriented and procedural programs.

A program profile attributes run-time costs to portions of a program's execution. Most profiling systems suffer from two major deficiencies: first, they only apportion simple metrics, such as execution frequency or elapsed time to static, syntactic units, such as procedures or statements; second, they aggressively reduce the volume of information collected and reported, although aggregation can hide striking differences in program behavior.This paper addresses both concerns by exploiting the hardware counters available in most modern processors and by incorporating two concepts from data flow analysis--flow and context sensitivity--to report more context for measurements. This paper extends our previous work on efficient path profiling to flow sensitive profiling, which associates hardware performance metrics with a path through a procedure. In addition, it describes a data structure, the calling context tree, that efficiently captures calling contexts for procedure-level measurements.Our measurements show that the SPEC95 benchmarks execute a small number (3--28) of hot paths that account for 9--98% of their L1 data cache misses. Moreover, these hot paths are concentrated in a few routines, which have complex dynamic behavior.

A path profile determines how many times each acyclic path in a routine executes. This type of profiling subsumes the more common basic block and edge profiling, which only approximate path frequencies. Path profiles have many potential uses in program performance tuning, profile-directed compilation, and software test coverage. This paper describes a new algorithm for path profiling. This simple, fast algorithm selects and places profile instrumentation to minimize run-time overhead. Instrumented programs run with overhead comparable to the best previous profiling techniques. On the SPEC95 benchmarks, path profiling overhead averaged 31%, as compared to 16% for efficient edge profiling. Path profiling also identifies longer paths than a previous technique, which predicted paths from edge profiles (average of 88, versus 34 instructions). Moreover, profiling shows that the SPEC95 train input datasets covered most of the paths executed in the ref datasets.

Recent research has offered programmers increased options for programming parallel computers by exposing system policies (e.g., memory coherence protocols) or by providing several programming paradigms (e.g. message passing and shared memory) on the same platform. Increased flexibility can lead to higher performance, but it is also a double-edged sword that demands a programmer understand his or her application and system at a more fundamental level. Our system, Tempest, allows a programmer to select or implement communication and memory coherence policies that fit an application's communication patterns. With it, we have achieved substantial performance gains without making major changes in programs. However, the process of selecting, designing, and implementing coherence protocols is difficult and time consuming, without tools to supply detailed information about an application's behavior and interaction with the memory system. StormWatch is a new visualization tool that aids a programmer through four mechanisms: tightly-coupled bidirectionally linked views, interactive filters, animation, and performance slicing. Multiple views present several aspects of program behavior simultaneously and show the same phenomenon from different perspectives. Real-time linking between views enables a programmer to explore levels of abstraction by changing a view and observing the effect on other views. Interactive filters, along with bidirectional linking, can isolate the effects of statements, loops, procedures, or files. StormWatch can also animate a program's dynamic behavior to show the evolution of program execution and communication. Finally, performance slicing captures causality among events. The examples in the paper illustrate how StormWatch helped us substantially improve the performance of two applications.

Abstract Inserting instrumentation code in a program is an effective technique for detecting, recording, and measuring many aspects of a program's performance. Instrumentation code can be added at any stage of the compilation process by specially‐modified system tools such as a compiler or linker or by new tools from a measurement system. For several reasons, adding instrumentation code after the compilation process—by rewriting the executable file—presents fewer complications and leads to more complete measurements. This paper describes the difficulties in adding code to executable files that arose in developing the profiling and tracing tools qp and qpt. The techniques used by these tools to instrument programs on MIPS and SPARC processors are applicable in other instrumentation systems running on many processors and operating systems. In addition, many difficulties could have been avoided with minor changes to compilers and executable file formats. These changes would simplify this approach to measuring program performance and make it more generally useful.

The ability to count events in a program's execution is required by many program analysis applications. We represent an instrumentation method for efficiently counting events in a program's execution, with support for on-line queries of the event count. Event counting differs from basic block profiling in that an aggregate count of events is kept rather than a set of counters. Due to this difference, solutions to basic block profiling are not well suited to event counting. Our algorithm finds a subset of points in a program to instrument, while guaranteeing that accurate event counts can be obtained efficiently at every point in the execution.

This paper describes algorithms for inserting monitoring code to profile and trace programs. These algorithms greatly reduce the cost of measuring programs with respect to the commonly used technique of placing code in each basic block. Program profiling counts the number of times each basic block in a program executes. Instruction tracing records the sequence of basic blocks traversed in a program execution. The algorithms optimize the placement of counting/tracing code with respect to the expected or measured frequency of each block or edge in a program's control-flow graph. We have implemented the algorithms in a profiling/tracing tool, and they substantially reduce the overhead of profiling and tracing. We also define and study the hierarchy of profiling problems. These problems have two dimensions: what is profiled (i.e., vertices (basic blocks) or edges in a control-flow graph) and where the instrumentation code is placed (in blocks or along edges). We compare the optimal solutions to the profiling problems and describe a new profiling problem: basic-block profiling with edge counters. This problem is important because an optimal solution to any other profiling problem (for a given control-flow graph) is never better than an optimal solution to this problem. Unfortunately, finding an optimal placement of edge counters for vertex profiling appears to be a hard problem in general. However, our work shows that edge profiling with edge counters works well in practice because it is simple and efficient and finds optimal counter placements in most cases. Furthermore, it yields more information than a vertex profile. Tracing also benefits from placing instrumentation code along edges rather than on vertices.

Many compilers rely on branch prediction to improve program performance by identifying frequently executed regions and by aiding in scheduling instructions.Profile-based predictors require a time-consuming and inconvenient compile-profile-compile cycle in order to make predictions. We present a program-based branch predictor that performs well for a large and diverse set of programs written in C and Fortran. In addition to using natural loop analysis to predict branches that control the iteration of loops, we focus on heuristics for predicting non-loop branches, which dominate the dynamic branch count of many programs. The heuristics are simple and require little program analysis, yet they are effective in terms of coverage and miss rate. Although program-based prediction does not equal the accuracy of profile-based prediction, we believe it reaches a sufficiently high level to be useful. Additional type and semantic information available to a compiler would enhance our heuristics.

This paper describes algorithms for inserting monitoring code to profile and trace programs. These algorithms greatly reduce the cost of measuring programs with respect to the commonly used technique of placing code in each basic block. Program profiling counts the number of times each basic block in a program executes. Instruction tracing records the sequence of basic blocks traversed in a program execution. The algorithms optimize the placement of counting/tracing code with respect to the expected or measured frequency of each block or edge in a program's control-flow graph. We have implemented the algorithms in a profiling/tracing tool, and they substantially reduce the overhead of profiling and tracing.We also define and study the hierarchy of profiling problems. These problems have two dimensions: what is profiled (i.e., vertices (basic blocks) or edges in a control-flow graph) and where the instrumentation code is placed (in blocks or along edges). We compare the optimal solutions to the profiling problems and describe a new profiling problem: basic-block profiling with edge counters. This problem is important because an optimal solution to any other profiling problem (for a given control-flow graph) is never better than an optimal solution to this problem. Unfortunately, finding an optimal placement of edge counters for vertex profiling appears to be a hard problem in general. However, our work shows that edge profiling with edge counters works well in practice because it is simple and efficient and finds optimal counter placements in most cases. Furthermore, it yields more information than a vertex profile. Tracing also benefits from placing instrumentation code along edges rather than on vertices.