SPLASH Companion 2016 – Author Index |
Contents -
Abstracts -
Authors
|
B C D E G H J K L M N P R S T V W Z
Bach, Christoph Tobias |
![]() Martin Alexander Neumann, Christoph Tobias Bach, Stefan Kratochwil, Marcel Kost, and Michael Beigl (KIT, Germany) Dynamically linked libraries such as libssl, libxml or libpam are in widespread use in server applications. Fixes to these libraries are released frequently, with security critical ones being among them few times each year--for example, to fix remote code execution. Such updates require applications to restart to make the dynamic linker effectively load the fix into the application. This is challenged by uptime-sensitive services leading to delayed installation of security patches and long periods of vulnerability. Current approaches to hot fixing such services allow instant replacement of functions. We discuss that security critical updates also affect data and present an approach for dynamically updating code and data in stock dynamically linked libraries in ELF format on Linux. The approach does not require source code access nor is preparation of applications ahead-of-time necessary, for example by code instrumentation. It uses the debugging symbols of all involved dynamic shared objects only. ![]() |
|
Barthels, Henrik |
![]() Henrik Barthels (RWTH Aachen University, Germany) In this paper we present a compiler that translates arithmetic expressions containing matrices to efficient sequences of calls to basic linear algebra kernels. ![]() |
|
Barzilay, Regina |
![]() Yewen Pu, Karthik Narasimhan, Armando Solar-Lezama, and Regina Barzilay (Massachusetts Institute of Technology, USA) We present a novel technique for automatic program correction in MOOCs, capable of fixing both syntactic and semantic errors without manual, problem specific correction strategies. Given an incorrect student program, it generates candidate programs from a distribution of likely corrections, and checks each candidate for correctness against a test suite. The key observation is that in MOOCs many programs share similar code fragments, and the seq2seq neural network model, used in the natural-language processing task of machine translation, can be modified and trained to recover these fragments. Experiment shows our scheme can correct 29% of all incorrect submissions and out-performs state of the art approach which requires manual, problem specific correction strategies. ![]() |
|
Beigl, Michael |
![]() Martin Alexander Neumann, Christoph Tobias Bach, Stefan Kratochwil, Marcel Kost, and Michael Beigl (KIT, Germany) Dynamically linked libraries such as libssl, libxml or libpam are in widespread use in server applications. Fixes to these libraries are released frequently, with security critical ones being among them few times each year--for example, to fix remote code execution. Such updates require applications to restart to make the dynamic linker effectively load the fix into the application. This is challenged by uptime-sensitive services leading to delayed installation of security patches and long periods of vulnerability. Current approaches to hot fixing such services allow instant replacement of functions. We discuss that security critical updates also affect data and present an approach for dynamically updating code and data in stock dynamically linked libraries in ELF format on Linux. The approach does not require source code access nor is preparation of applications ahead-of-time necessary, for example by code instrumentation. It uses the debugging symbols of all involved dynamic shared objects only. ![]() |
|
Braz, Larissa |
![]() Larissa Braz (Federal University of Campina Grande, Brazil) Configurable systems typically use #ifdefs to denote variability. Generating and compiling all configurations may be time-consuming. An alternative consists of using variability-aware parsers, such as TypeChef. However, they may not scale. We propose a change-centric approach to compile configurable systems with #ifdefs by analyzing only configurations impacted by a code change. We implemented it in a tool called CHECKCONFIGMX. We perform an empirical study to evaluate 3,913 transformations applied to the 14 largest files of BusyBox, Apache HTTPD, and Expat configurable systems. CHECKCONFIGMX finds 595 compilation errors of 20 types introduced by 41 developers in 214 commits (5.46% of the analyzed transformations). In our study, it reduces by at least 50% (an average of 99%) the effort of evaluating the analyzed transformations by comparing with the exhaustive approach without considering a feature model. ![]() |
|
Buckley, Scott |
![]() Scott Buckley, Anthony Sloane, and Matthew Roberts (Macquarie University, Australia) Layout for web documents is a complex process described by the lengthy prose Cascading Style Sheets (CSS) specification. It is difficult to ensure that implementations match this specification. We show how an implementation can more closely match the specification by using attribute grammars to define layout computations. Particularly, we show how high-level patterns encode the terminology of the specification, discriminating between elements using the same language as in the specification. We also present a new method of injecting artificial structure into an existing tree using reference attribute grammars. The result is a high-level executable specification for CSS layout that can form the basis for a full declarative implementation. ![]() |
|
Caldwell, Joseph |
![]() Joseph Caldwell (University of Tokyo, Japan) The use of a standard calling convention throughout a binary can bloat code size and negatively impact power consumption, flash memory costs, and chip size in embedded or otherwise size-critical domains. This is particularly true in ”compressed” instruction sets, such as the 16-bit ARM Thumb instruction set, used in virtually all smart phones and in many other smaller-scale embedded devices. Here, we examine the extent of the problem in modern embedded software. We found that between 6-17% of the code in typical binaries represents overhead attributable to the calling convention. Finally, we propose a method of reducing this overhead by assigning calling conventions per-procedure during register allocation, and discuss solutions to scalability problems with this approach. ![]() |
|
Chang, David |
![]() David Chang, Thu Nguyen, and Niko Takayesu (Grinnell College, USA) Developers and compiler writers spend significant effort on performance tuning and optimizations. However, the impact of these efforts must be taken with a grain of salt. Prior work has shown that changes to a program's layout—the placement of code and data in memory—can change performance by more than the effect of standard optimization techniques. This paper presents Scrambler, a system that dynamically changes the layout of programs to improve their performance. Scrambler runs C and C++ programs with a randomized layout, and monitors these programs for evidence of layout-related performance issues. When an issue is detected, Scrambler relocates the offending code to eliminate the layout issue. We evaluate Scrambler on eight SPEC CPU2006 benchmarks, and find that Scrambler can provide speedups as large as 4.6% by fixing layouts that hurt branch predictor performance. These early results are encouraging, and we plan to extend this work to support additional layout-related performance issues in the future. ![]() |
|
Charousset, Dominik |
![]() Raphael Hiesgen, Dominik Charousset, and Thomas C. Schmidt (Hamburg University of Applied Sciences, Germany) Frameworks inspired by the actor model have recently attracted much attention. Actor systems promise transparent concurrency and distribution by combining message passing with a strong failure model. In this work, we re-examine distribution transparency and find that reliability breaks the promise in several dimensions. Solutions for regaining awareness of failures are briefly discussed. ![]() |
|
Cherayil, Jessica |
![]() Jessica Cherayil (Wellesley College, USA) Eye tracking studies are valuable for evaluating program- ming environments, but annotating what the programmer is looking at in a dynamic environment can be repetitive, time- consuming, and error prone. Through a participatory design exercise with two eye tracking researchers, I identified three significant challenges: search, extraction of code, and annotat- ing transient objects. By applying computer vision algorithms to video traces, I developed a mixed-initiative system called PIXELDUST, which allows the researcher to train a system to recognize different objects on a screen. My preliminary results demonstrate the versatility of the approach; for ex- ample, the system can recognize return statements, method signatures, tool tips, and dialog boxes. ![]() |
|
Chiş, Andrei |
![]() Andrei Chiş (University of Bern, Switzerland) Reasoning about object-oriented applications requires developers to answer contextual questions about their domain objects. Tailored development tools can support developers in this activity by providing relevant domain-specific information. Nonetheless, a high effort for extending development tools to handle domain-specific objects, together with diverging mechanisms for creating, sharing and discovering extensions, discourage developers to adapt their tools. To address this, we propose to enable contextual behavior in development tools by allowing domain objects to decide how they are handled in development tools. We show that combining this idea with mechanisms for specifying extensions using internal DSLs can significantly reduce the cost of tailoring development tools to specific domains. ![]() ![]() |
|
Dürschmid, Tobias |
![]() Tobias Dürschmid (HPI, Germany) Reuse is one of the core principles in professional software engineering. Design patterns provide a reusable solution for common design problems. But their implementations are generally not reusable as they are often well tailored to a specific context. We introduce a concept, that facilitates the reuse of their implementations by defining an abstract design pattern definition that can be instantiated with specialized design decisions. This approach is a meta-level Builder constructing design patterns as first-class citizens. It simplifies the application of design patterns by providing a pattern library and still being able to adjust it to the concrete context. ![]() |
|
Eichholz, Matthias |
![]() Matthias Eichholz (TU Darmstadt, Germany) Programming languages for Software-Defined Networks (SDNs) provide higher abstractions on top of hardware-based APIs like OpenFlow. Researchers started to develop SDN programming languages based on mathematical foundations, which makes these languages amenable to verification and allows network administrators to answer questions about correctness of their policies, reachability within the network and performance of the network. However, these languages are only able to capture a limited set of properties and lack support for fully automated verification. In this paper we first highlight different issues of existing programming languages enabling network verification for SDNs and describe ongoing research on a new SDN language that tackles the aforementioned issues. ![]() |
|
Erich, Floris |
![]() Floris Erich (University of Tsukuba, Japan) Robots understand the world around them through sensing. To process the data produced by sensors we propose to use Procedural Parameters and Complex Event Processing (CEP). End-users model applications for robots as a CEP Graph, in which the end-users specify how input from the sensors of the robot is transformed to output for the actuators of the robot. Between input and output is a network of streams connected together by operators. By using Procedural Parameters a set of generic operators can be used within the CEP Graph. The CEP Graph can be executed on the robot or on a PC remotely controlling the robot. ![]() |
|
Etzel, Tyler |
![]() Tyler Etzel (Cornell University, USA) Immutability is a valuable feature for programmers in object-oriented languages: making objects immutable often simplifies reasoning about the correctness of code, particularly when concurrency is present. Java allows programmers to express and enforce immutability by declaring all fields of an object "final", but this comes at the cost of decreased expressiveness and intuitiveness of initialization. In this work, we propose a minimalistic type-based mechanism that both enforces immutability and relaxes these constraints on initialization. Furthermore, we propose and formalize two different type systems based on this mechanism that form a meaningful trade-off with respect to complexity, expressiveness, and strength of static guarantees. System One is simple, more expressive, and provides object-level immutability; System Two has more complicated annotation, is less expressive, and ensures that immutable objects are fully initialized in addition to enforcing immutability. ![]() |
|
Goldberg, Logan |
![]() Logan Goldberg, Joel Katticaran, and Abraham Mhaidli (Grinnell College, USA) Rapid increases in demand for cloud computing, large-scale internet services, and mobile devices have led to a correspondingly large increase in the amount of energy required for computation. This additional energy use comes at a high cost, both financially and environmentally. Energy profilers are useful tools which allow programmers to energy audit their programs and determine what functions are responsible for the most energy use. In this paper, we introduce a new technique for energy profiling, which takes energy measurements at regularly spaced intervals and uses linear regression to correlate executing functions with changes in power demand. We have implemented this technique in Alpaca, an energy profiler for Linux. Initial results suggest that this approach shows promise in energy profiling programs in an accurate and meaningful way. ![]() |
|
Grandi, Marco |
![]() Marco Grandi (University of Pisa, Italy) Persistence and distribution are two important aspects in distributed applications that are commonly managed explicitly and separately. This paper introduces Spray, a programming paradigm for distributed applications that combines these two concepts in one abstraction: a persistent distributed heap. ![]() |
|
Grewe, Sylvia |
![]() Sylvia Grewe (TU Darmstadt, Germany) Developing a type system with a soundness proof is hard. The VeriTaS project aims at simplifying the development of sound type systems through automation of soundness proofs and through automated derivation of efficient type checkers from sound type system specifications. Within the VertiTaS project, I focus on developing an interface for the verification of progress and preservation proofs which shall automate standard parts of such proofs. To achieve this, I propose to identify recurring proof strategies in progress and preservation proofs from the literature, to develop a format for abstractly representing these proof strategies, and to mechanize them by connecting them to existing theorem provers. ![]() |
|
Habib, Andrew |
![]() Andrew Habib (TU Darmstadt, Germany) Concurrency bugs are very difficult and subtle to discover, reproduce, and fix. Many techniques have been devised by the academic as well as the industry communities to find these bugs. However, most of the effective techniques tend to focus on a subset of the various concurrency bugs types. We propose a new generic concurrency bug detection technique that leverages "Big Code": millions of lines of code freely available on code repositories. Our approach tries to learn the properties of what constitutes a good and a bad synchronization pattern from hundreds of concurrent software using graph-based anomaly detection. ![]() |
|
Hiesgen, Raphael |
![]() Raphael Hiesgen, Dominik Charousset, and Thomas C. Schmidt (Hamburg University of Applied Sciences, Germany) Frameworks inspired by the actor model have recently attracted much attention. Actor systems promise transparent concurrency and distribution by combining message passing with a strong failure model. In this work, we re-examine distribution transparency and find that reliability breaks the promise in several dimensions. Solutions for regaining awareness of failures are briefly discussed. ![]() |
|
Jamali, Nadeem |
![]() Ahmed Abdel Moamen and Nadeem Jamali (University of Saskatchewan, Canada) There are several advantages of multitenancy: the serving of multiple tenants, each with its own privileges, from the same instance of a software system. Although the naming convention in actor systems -- actor names cannot be guessed -- naturally supports multitenancy, there is no explicit way of managing the resource competition between tenants. There are models for coordinating resource use in actor systems; however, they are difficult to implement for efficient implementations of Actors. This paper presents our efforts in implementing resource coordination support for actor systems implemented using the Akka library. ![]() |
|
Juhár, Ján |
![]() Ján Juhár (Technical University of Košice, Slovakia) Program comprehension is an essential process in programming and many researchers report that it tends to take up to a half of a programmers' time during their work with a source code. Integrated development environments (IDEs) facilitate this process but there still are only restricted possibilities for narrowing the gap between concerns of a problem domain and a source code that implements them. In our work we utilize projectional properties of modern IDEs to make them able to process concern-related metadata and to provide customizable code projections. These projections preserve the original code structure while they show it from an alternative perspective regarding the contained concerns. We plan to evaluate the effect such code projections will have on program comprehension tasks. ![]() |
|
Kamina, Tetsuo |
![]() Tetsuo Kamina (Ritsumeikan University, Japan) This paper introduces SignalJ, a lightweight extension of Java with reactive values. A reactive value is a value that can depend on other reactive values, and it is implicitly updated when the depended reactive values are updated. Each reactive value is typed with a signal type, which ensures that the dependent reactive values are functional. SignalJ also provides handlers of reactive values that are called whenever the monitored reactive value is updated. With these features, SignalJ declaratively specifies dataflows within an application in a functional manner, which enables effective implementation of reactive software. The syntax of SignalJ is almost identical to that of Java 8 except that it introduces a new modifier, signal, to represent signal types. ![]() |
|
Katticaran, Joel |
![]() Logan Goldberg, Joel Katticaran, and Abraham Mhaidli (Grinnell College, USA) Rapid increases in demand for cloud computing, large-scale internet services, and mobile devices have led to a correspondingly large increase in the amount of energy required for computation. This additional energy use comes at a high cost, both financially and environmentally. Energy profilers are useful tools which allow programmers to energy audit their programs and determine what functions are responsible for the most energy use. In this paper, we introduce a new technique for energy profiling, which takes energy measurements at regularly spaced intervals and uses linear regression to correlate executing functions with changes in power demand. We have implemented this technique in Alpaca, an energy profiler for Linux. Initial results suggest that this approach shows promise in energy profiling programs in an accurate and meaningful way. ![]() |
|
Ko, Andrew |
![]() Andrew Ko (University of Washington, USA) In computer science, we usually take a technical view of programming languages, defining them as precise, formal ways of specifying a computer behavior. This view shapes much of the research and development that we do on programming languages, determining the questions we ask about them, the improvements we make to them, and how we teach people to use them. But to many people (even software engineers) programming languages are not purely technical things, but socio-technical things. In this talk, I discuss several alternative views of programming languages, and how these views can reshape how we design, evolve, and use programming languages in research and practice. ![]() |
|
Kost, Marcel |
![]() Martin Alexander Neumann, Christoph Tobias Bach, Stefan Kratochwil, Marcel Kost, and Michael Beigl (KIT, Germany) Dynamically linked libraries such as libssl, libxml or libpam are in widespread use in server applications. Fixes to these libraries are released frequently, with security critical ones being among them few times each year--for example, to fix remote code execution. Such updates require applications to restart to make the dynamic linker effectively load the fix into the application. This is challenged by uptime-sensitive services leading to delayed installation of security patches and long periods of vulnerability. Current approaches to hot fixing such services allow instant replacement of functions. We discuss that security critical updates also affect data and present an approach for dynamically updating code and data in stock dynamically linked libraries in ELF format on Linux. The approach does not require source code access nor is preparation of applications ahead-of-time necessary, for example by code instrumentation. It uses the debugging symbols of all involved dynamic shared objects only. ![]() |
|
Kratochwil, Stefan |
![]() Martin Alexander Neumann, Christoph Tobias Bach, Stefan Kratochwil, Marcel Kost, and Michael Beigl (KIT, Germany) Dynamically linked libraries such as libssl, libxml or libpam are in widespread use in server applications. Fixes to these libraries are released frequently, with security critical ones being among them few times each year--for example, to fix remote code execution. Such updates require applications to restart to make the dynamic linker effectively load the fix into the application. This is challenged by uptime-sensitive services leading to delayed installation of security patches and long periods of vulnerability. Current approaches to hot fixing such services allow instant replacement of functions. We discuss that security critical updates also affect data and present an approach for dynamically updating code and data in stock dynamically linked libraries in ELF format on Linux. The approach does not require source code access nor is preparation of applications ahead-of-time necessary, for example by code instrumentation. It uses the debugging symbols of all involved dynamic shared objects only. ![]() |
|
Leske, Max |
![]() Max Leske (University of Bern, Switzerland) Contemporary live debuggers do not display the complete call stack history for concurrent threads. Hence, developers have less information at their disposal when debugging concurrent threads than when debugging a single threaded, sequential program. We solve the problem of incomplete thread history by creating a debugger that operates on a virtual call stack comprised of multiple threads. With live debuggers displaying at least the equivalent information for both single threaded, sequential programs and concurrent threads, developers can focus on the hard parts of concurrency issues. ![]() |
|
Lorenz, David H. |
![]() David H. Lorenz and Boaz Rosenan (Open University of Israel, Israel; Technion, Israel; University of Haifa, Israel) We introduce a correspondence between the design space of web applications and that of domain-specific languages (DSLs). We note that while most web applications today are implemented in ways that correspond to external DSLs, very little attention is given to implementation techniques corresponding to internal DSLs. We contribute a technique based on internal DSLs, and demonstrate a web application implemented with our technique. ![]() |
|
Mhaidli, Abraham |
![]() Logan Goldberg, Joel Katticaran, and Abraham Mhaidli (Grinnell College, USA) Rapid increases in demand for cloud computing, large-scale internet services, and mobile devices have led to a correspondingly large increase in the amount of energy required for computation. This additional energy use comes at a high cost, both financially and environmentally. Energy profilers are useful tools which allow programmers to energy audit their programs and determine what functions are responsible for the most energy use. In this paper, we introduce a new technique for energy profiling, which takes energy measurements at regularly spaced intervals and uses linear regression to correlate executing functions with changes in power demand. We have implemented this technique in Alpaca, an energy profiler for Linux. Initial results suggest that this approach shows promise in energy profiling programs in an accurate and meaningful way. ![]() |
|
Moamen, Ahmed Abdel |
![]() Ahmed Abdel Moamen and Nadeem Jamali (University of Saskatchewan, Canada) There are several advantages of multitenancy: the serving of multiple tenants, each with its own privileges, from the same instance of a software system. Although the naming convention in actor systems -- actor names cannot be guessed -- naturally supports multitenancy, there is no explicit way of managing the resource competition between tenants. There are models for coordinating resource use in actor systems; however, they are difficult to implement for efficient implementations of Actors. This paper presents our efforts in implementing resource coordination support for actor systems implemented using the Akka library. ![]() |
|
Mongiovi, Melina |
![]() Melina Mongiovi (Federal University of Campina Grande, Brazil) Refactoring engines may have overly weak conditions, overly strong conditions, and transformation issues related to the refactoring definitions. We find that 86% of the test suites of Eclipse and JRRT are concerned to those kinds of bugs. However, the engines still have them. Researchers have proposed a number of techniques for testing refactoring engines. Nevertheless, they may have limitations related to the program generator, time consumption, kinds of bugs, automation, and debugging. We propose and implement a technique to scale testing of refactoring engines. We improve expressiveness of a program generator and use a technique to skip some test inputs to improve performance. Moreover, we propose new oracles to detect behavioral changes using change impact analysis, overly strong conditions using mutation testing, and transformation issues. We evaluate our technique in 28 refactoring implementations of Java (Eclipse and JRRT) and C (Eclipse) and find 119 bugs. The technique reduces the time in 96% using skips while missing only 6% of the bugs. Using the new oracle to identify overly strong conditions, it detects more bugs and facilitates the debugging activity different from previous works. Finally, we evaluate refactoring implementations of Eclipse and JRRT using the input programs of their refactoring test suites and find a number of bugs not detected by the developers. ![]() |
|
Murphy, Gail C. |
![]() Giovanni Viviani and Gail C. Murphy (University of British Columbia, Canada) Finding defects efficently is one of the major problems in software development, a problem that often still relies largely on human inspection of code to find defects. Many software development projects use code reviews as a mean to ensure this human inspection occurs. Known as modern code review, this approach is based on tools, such as Gerrit, that help the developers in the reviewing process. As part of this approach, developers are often presented with a list of open code reviews requiring attention; it is left to the developer to find a suitable review on which to work on from a long list of reviews. We present an investigation of two algorithms that recommend an ordering of the list of open reviews based on properties of the reviews. We use a simulation study over the JGit project from the Eclipse Foundation to show that an algorithm based on ordering reviews from least lines of codes changed in the code review to most lines of code out performs other algorithms. This algorithm shows promise for eliminating stagnation of reviews and optimizing the average duration reviews are open. ![]() |
|
Narasimhan, Karthik |
![]() Yewen Pu, Karthik Narasimhan, Armando Solar-Lezama, and Regina Barzilay (Massachusetts Institute of Technology, USA) We present a novel technique for automatic program correction in MOOCs, capable of fixing both syntactic and semantic errors without manual, problem specific correction strategies. Given an incorrect student program, it generates candidate programs from a distribution of likely corrections, and checks each candidate for correctness against a test suite. The key observation is that in MOOCs many programs share similar code fragments, and the seq2seq neural network model, used in the natural-language processing task of machine translation, can be modified and trained to recover these fragments. Experiment shows our scheme can correct 29% of all incorrect submissions and out-performs state of the art approach which requires manual, problem specific correction strategies. ![]() |
|
Neumann, Martin Alexander |
![]() Martin Alexander Neumann (KIT, Germany) Towards more usable dynamic software updating on stock Java, we propose (1) a programming model that transformation code can be statically type-checked against, also featuring type-safe execution of transformation code; (2) an efficient checkpointable eager state transformation approach that avoids hazards of deadlocks and data-races when transformation code is executed, also allowing to seamlessly abort an update if any exception occurs; and (3) a programming approach based on assertions to abort dynamic updates if assumptions of transformation code are not met. We implement the three aspects in a dynamic updating system to study their performance and usability. ![]() ![]() Martin Alexander Neumann, Christoph Tobias Bach, Stefan Kratochwil, Marcel Kost, and Michael Beigl (KIT, Germany) Dynamically linked libraries such as libssl, libxml or libpam are in widespread use in server applications. Fixes to these libraries are released frequently, with security critical ones being among them few times each year--for example, to fix remote code execution. Such updates require applications to restart to make the dynamic linker effectively load the fix into the application. This is challenged by uptime-sensitive services leading to delayed installation of security patches and long periods of vulnerability. Current approaches to hot fixing such services allow instant replacement of functions. We discuss that security critical updates also affect data and present an approach for dynamically updating code and data in stock dynamically linked libraries in ELF format on Linux. The approach does not require source code access nor is preparation of applications ahead-of-time necessary, for example by code instrumentation. It uses the debugging symbols of all involved dynamic shared objects only. ![]() |
|
Nguyen, Thu |
![]() David Chang, Thu Nguyen, and Niko Takayesu (Grinnell College, USA) Developers and compiler writers spend significant effort on performance tuning and optimizations. However, the impact of these efforts must be taken with a grain of salt. Prior work has shown that changes to a program's layout—the placement of code and data in memory—can change performance by more than the effect of standard optimization techniques. This paper presents Scrambler, a system that dynamically changes the layout of programs to improve their performance. Scrambler runs C and C++ programs with a randomized layout, and monitors these programs for evidence of layout-related performance issues. When an issue is detected, Scrambler relocates the offending code to eliminate the layout issue. We evaluate Scrambler on eight SPEC CPU2006 benchmarks, and find that Scrambler can provide speedups as large as 4.6% by fixing layouts that hurt branch predictor performance. These early results are encouraging, and we plan to extend this work to support additional layout-related performance issues in the future. ![]() |
|
Pierce, Benjamin C. |
![]() Benjamin C. Pierce (University of Pennsylvania, USA) Abstraction and modularity underlie all successful hardware and software systems: We build complex artifacts by decomposing them into parts that can be understood separately. Modular decomposition depends crucially on the artful choice of interfaces between pieces. As these interfaces become more expressive, we think of them as specifications of components or layers. Rich specifications based on formal logic are little used in industry today, but a practical platform for working with them could signicantly reduce the costs of system implementation and evolution by identifying vulnerabilities, helping programmers understand the behavior of new components, facilitating rigorous change-impact analysis, and supporting maintainable machine-checked verication that components are correct and fit together correctly. Recently, research in the area has begun to focus on a particularly rich class of specifications, which might be called deep specifications. Deep specifications are rich (describing complex component behaviors in detail); two-sided (connected to both implementations and clients); formal (written in a mathematical notation with clear semantics to support tools such as type checkers, analysis and testing tools, automated or machine-assisted provers, and advanced IDEs); and live (connected directly to the source code of implementations via machine-checkable proofs or property-based random testing). These requirements impose strong functional correctness conditions on individual components and permit them to be connected together with rigorous composition theorems. This talk presents the key features of deep specifications, surveys recent achievements and ongoing efforts in the research community (in particular, work at Penn, Princeton, Yale, and MIT on formalizing a rich interconnected collection of deep specifications for critical system software components), and argues that the time is ripe for an intensive effort in this area, involving both academia and industry and integrating research, education, and community building. The ultimate goal is to provide rigorously checked proofs about much larger artifacts than are feasible today, based on decomposition of proof effort across components with deep specifications. ![]() |
|
Pu, Yewen |
![]() Yewen Pu, Karthik Narasimhan, Armando Solar-Lezama, and Regina Barzilay (Massachusetts Institute of Technology, USA) We present a novel technique for automatic program correction in MOOCs, capable of fixing both syntactic and semantic errors without manual, problem specific correction strategies. Given an incorrect student program, it generates candidate programs from a distribution of likely corrections, and checks each candidate for correctness against a test suite. The key observation is that in MOOCs many programs share similar code fragments, and the seq2seq neural network model, used in the natural-language processing task of machine translation, can be modified and trained to recover these fragments. Experiment shows our scheme can correct 29% of all incorrect submissions and out-performs state of the art approach which requires manual, problem specific correction strategies. ![]() |
|
Rein, Patrick |
![]() Patrick Rein (HPI, Germany) The interoperability of applications depends on a successful mapping between their domain models. Nowadays, common file formats serve as a mediator between the different domain models but cause friction losses during the conversion of data. These loses could be mitigated whenever the models are already working on the same concepts but are only using different representations for them. We propose the concept of deducing classes which interpret existing object structures and detect instances of themselves in this existing data. Further, we introduce a planning algorithm which combines deducing classes to allow unanticipated interactions between applications. We discuss some of the implications of this approach and illustrate upcoming research challenges. ![]() |
|
Roberts, Matthew |
![]() Scott Buckley, Anthony Sloane, and Matthew Roberts (Macquarie University, Australia) Layout for web documents is a complex process described by the lengthy prose Cascading Style Sheets (CSS) specification. It is difficult to ensure that implementations match this specification. We show how an implementation can more closely match the specification by using attribute grammars to define layout computations. Particularly, we show how high-level patterns encode the terminology of the specification, discriminating between elements using the same language as in the specification. We also present a new method of injecting artificial structure into an existing tree using reference attribute grammars. The result is a high-level executable specification for CSS layout that can form the basis for a full declarative implementation. ![]() |
|
Rosenan, Boaz |
![]() David H. Lorenz and Boaz Rosenan (Open University of Israel, Israel; Technion, Israel; University of Haifa, Israel) We introduce a correspondence between the design space of web applications and that of domain-specific languages (DSLs). We note that while most web applications today are implemented in ways that correspond to external DSLs, very little attention is given to implementation techniques corresponding to internal DSLs. We contribute a technique based on internal DSLs, and demonstrate a web application implemented with our technique. ![]() |
|
Schkufza, Eric |
![]() Tal Wagner, Eric Schkufza, and Udi Wieder (Massachusetts Institute of Technology, USA; VMware, USA) Log management systems are common in industry and an essential part of a system administrator’s toolkit. Examples include Splunk, elk, Log Insight, Sexilog, and more. Logs in these systems are characterized by a small number of predefined fields such as timestamp and host, with the bulk of an entry being unstructured text. System administrators query these logs using a combination of range constraints over predefined fields and patterns or regular expressions over the text portion of the message. These queries are both complex and diverse. We propose a method for maintaining a subset of these logs in a much smaller database known as a sublog. Because queries are issued against a much smaller data set they run to completion quickly and avoid common scaling bottlenecks. However, the improvement in performance comes at a price. Because we only consider a subset of the original data, we are only able to provide approximate responses. Nonetheless, the reduction in accuracy is minimal and we are able to produce high-quality, high-performance results. ![]() |
|
Schmidt, Thomas C. |
![]() Raphael Hiesgen, Dominik Charousset, and Thomas C. Schmidt (Hamburg University of Applied Sciences, Germany) Frameworks inspired by the actor model have recently attracted much attention. Actor systems promise transparent concurrency and distribution by combining message passing with a strong failure model. In this work, we re-examine distribution transparency and find that reliability breaks the promise in several dimensions. Solutions for regaining awareness of failures are briefly discussed. ![]() |
|
Sloane, Anthony |
![]() Scott Buckley, Anthony Sloane, and Matthew Roberts (Macquarie University, Australia) Layout for web documents is a complex process described by the lengthy prose Cascading Style Sheets (CSS) specification. It is difficult to ensure that implementations match this specification. We show how an implementation can more closely match the specification by using attribute grammars to define layout computations. Particularly, we show how high-level patterns encode the terminology of the specification, discriminating between elements using the same language as in the specification. We also present a new method of injecting artificial structure into an existing tree using reference attribute grammars. The result is a high-level executable specification for CSS layout that can form the basis for a full declarative implementation. ![]() |
|
Solar-Lezama, Armando |
![]() Yewen Pu, Karthik Narasimhan, Armando Solar-Lezama, and Regina Barzilay (Massachusetts Institute of Technology, USA) We present a novel technique for automatic program correction in MOOCs, capable of fixing both syntactic and semantic errors without manual, problem specific correction strategies. Given an incorrect student program, it generates candidate programs from a distribution of likely corrections, and checks each candidate for correctness against a test suite. The key observation is that in MOOCs many programs share similar code fragments, and the seq2seq neural network model, used in the natural-language processing task of machine translation, can be modified and trained to recover these fragments. Experiment shows our scheme can correct 29% of all incorrect submissions and out-performs state of the art approach which requires manual, problem specific correction strategies. ![]() |
|
Szabó, Tamás |
![]() Tamás Szabó (itemis, Germany; Delft University of Technology, Netherlands) Language workbenches are widely used to implement domain-specific languages (DSLs) and their accompanying integrated development environments (IDEs). They help to define the abstract syntax, concrete syntax(es), type system, and transformations for the languages. However, there are other language aspects, specifically program analyses and optimizations, that are also crucial to a language implementation, but state-of-the-art language workbenches has only limited support for them. The high implementation effort for these language aspects is justifiable for a general-purpose language (GPL), but is not justifiable for DSLs because of their different development economies. To this end, I conduct research on dedicated support for analyses and optimizations for DSLs in language workbenches. My main goal is to develop declarative meta-languages that help to define static program analyses and that capture and automate patterns and techniques of optimizations. The research directions are directly driven by industrial need, and upon successful completion, the results would be applied in projects centered around DSLs for high-performance computing (HPC), insurance, and concurrent embedded systems. ![]() |
|
Takayesu, Niko |
![]() David Chang, Thu Nguyen, and Niko Takayesu (Grinnell College, USA) Developers and compiler writers spend significant effort on performance tuning and optimizations. However, the impact of these efforts must be taken with a grain of salt. Prior work has shown that changes to a program's layout—the placement of code and data in memory—can change performance by more than the effect of standard optimization techniques. This paper presents Scrambler, a system that dynamically changes the layout of programs to improve their performance. Scrambler runs C and C++ programs with a randomized layout, and monitors these programs for evidence of layout-related performance issues. When an issue is detected, Scrambler relocates the offending code to eliminate the layout issue. We evaluate Scrambler on eight SPEC CPU2006 benchmarks, and find that Scrambler can provide speedups as large as 4.6% by fixing layouts that hurt branch predictor performance. These early results are encouraging, and we plan to extend this work to support additional layout-related performance issues in the future. ![]() |
|
Viviani, Giovanni |
![]() Giovanni Viviani and Gail C. Murphy (University of British Columbia, Canada) Finding defects efficently is one of the major problems in software development, a problem that often still relies largely on human inspection of code to find defects. Many software development projects use code reviews as a mean to ensure this human inspection occurs. Known as modern code review, this approach is based on tools, such as Gerrit, that help the developers in the reviewing process. As part of this approach, developers are often presented with a list of open code reviews requiring attention; it is left to the developer to find a suitable review on which to work on from a long list of reviews. We present an investigation of two algorithms that recommend an ordering of the list of open reviews based on properties of the reviews. We use a simulation study over the JGit project from the Eclipse Foundation to show that an algorithm based on ordering reviews from least lines of codes changed in the code review to most lines of code out performs other algorithms. This algorithm shows promise for eliminating stagnation of reviews and optimizing the average duration reviews are open. ![]() |
|
Wagner, Tal |
![]() Tal Wagner, Eric Schkufza, and Udi Wieder (Massachusetts Institute of Technology, USA; VMware, USA) Log management systems are common in industry and an essential part of a system administrator’s toolkit. Examples include Splunk, elk, Log Insight, Sexilog, and more. Logs in these systems are characterized by a small number of predefined fields such as timestamp and host, with the bulk of an entry being unstructured text. System administrators query these logs using a combination of range constraints over predefined fields and patterns or regular expressions over the text portion of the message. These queries are both complex and diverse. We propose a method for maintaining a subset of these logs in a much smaller database known as a sublog. Because queries are issued against a much smaller data set they run to completion quickly and avoid common scaling bottlenecks. However, the improvement in performance comes at a price. Because we only consider a subset of the original data, we are only able to provide approximate responses. Nonetheless, the reduction in accuracy is minimal and we are able to produce high-quality, high-performance results. ![]() |
|
Weisenburger, Pascal |
![]() Pascal Weisenburger (TU Darmstadt, Germany) Distributed applications are traditionally developed using separate modules for each component in the distributed system, which can even be written in different programming languages. Those modules react on events such as user input, which are produced by other modules, and may in turn produce new events to be handled by different modules. Thus, most distributed applications are reactive in nature. Distributed event-based data flow makes it is hard to reason about the system and therefore makes the development of distributed systems challenging. In this paper, we present language abstractions for distributed reactive programming easing the development of such applications and supporting various distributed architectures. ![]() |
|
Wieder, Udi |
![]() Tal Wagner, Eric Schkufza, and Udi Wieder (Massachusetts Institute of Technology, USA; VMware, USA) Log management systems are common in industry and an essential part of a system administrator’s toolkit. Examples include Splunk, elk, Log Insight, Sexilog, and more. Logs in these systems are characterized by a small number of predefined fields such as timestamp and host, with the bulk of an entry being unstructured text. System administrators query these logs using a combination of range constraints over predefined fields and patterns or regular expressions over the text portion of the message. These queries are both complex and diverse. We propose a method for maintaining a subset of these logs in a much smaller database known as a sublog. Because queries are issued against a much smaller data set they run to completion quickly and avoid common scaling bottlenecks. However, the improvement in performance comes at a price. Because we only consider a subset of the original data, we are only able to provide approximate responses. Nonetheless, the reduction in accuracy is minimal and we are able to produce high-quality, high-performance results. ![]() |
|
Zhang, Zhen |
![]() Zhen Zhang (University of Science and Technology of China, China) JavaScript is the de facto language of the Web, but is notoriously error-prone to use. 65% of common bugs like undefined/null variable usage are DOM-related. Besides DOM, JS APIs are also expected to manipulate graphic hardware and asynchronous I/O, which makes the condition even worse. Although WebIDL provides a formal contract between JS developers and platform implementation, its expressivity is too limited to support deep checking of API misuses. We propose the eXtended WebIDL (xWIDL) language and a modular API misuses checking framework based on xWIDL. We discuss how to handle the data exchange between JS analyzer and SMT-based verifier. Finally, we test our implementation in a case study manner and report our findings on its efficiency and modularity. ![]() |
53 authors
proc time: 1.14