Powered by
2015 ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH Companion 2015),
October 25–30, 2015,
Pittsburgh, PA, USA
Student Research Competition
Efficient Support for Strong Semantics in Transactional and Non-transactional Programs
Aritra Sengupta
(Ohio State University, USA)
Transactional programs, using transactional memory (TM) and non-transactional programs (non-TM) (e.g., using locks) provide weak semantics under commonly used memory models. Strong memory models incur high implementation overhead and yet prove to be insufficient. TM programs and non-TM programs have different semantics based on the memory model. Adding new atomic blocks to lock-based code is difficult without adding high overhead or introducing weak semantics. A system where users can add atomic blocks or lock-based critical sections seamlessly to existing TM programs or lock-based code facilitates incremental deployment. A unified and strong memory model enforced efficiently by a single runtime for both kinds of programs is therefore desirable.
@InProceedings{SPLASH Companion15p67,
author = {Aritra Sengupta},
title = {Efficient Support for Strong Semantics in Transactional and Non-transactional Programs},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {67--68},
doi = {},
year = {2015},
}
Automatic Array Property Detection via Static Analysis
Alisa J. Maas
(University of Wisconsin-Madison, USA)
Simultaneous use of multiple programming languages aids in creating efficient modern programs in the face of legacy code; however, creating language bindings to low-level languages like C by hand is tedious and error prone. We offer an automated suite of analyses to enhance the quality of automatically produced bindings by recovering high-level array type information missing in C's type system. We emit annotations in the style of GObjectIntrospection, which produces bindings from annotations. We annotate an array argument as terminated by a special sentinel value, fixed length of a constant size, or of length determined by another argument. This information helps produce more idiomatic, efficient bindings.
@InProceedings{SPLASH Companion15p69,
author = {Alisa J. Maas},
title = {Automatic Array Property Detection via Static Analysis},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {69--70},
doi = {},
year = {2015},
}
KinEdit: A Tool to Help Developers Refactor Manually
Josh Terrell
(California Polytechnic State University, USA)
Some developers do not trust automated refactoring tools to refactor correctly. Refactoring without tools can be a cumbersome and error-prone process. It is possible for a tool to support developers in refactoring without requiring them to trust in automated code manipulation. This paper contributes KinEdit—a tool which is designed to help developers manually refactor more quickly, with higher quality, and without requiring the developers’ trust.
@InProceedings{SPLASH Companion15p71,
author = {Josh Terrell},
title = {KinEdit: A Tool to Help Developers Refactor Manually},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {71--72},
doi = {},
year = {2015},
}
Finding Bugs in Spreadsheets using Reference Counting
Nima Joharizadeh
(University of California at Davis, USA)
Spreadsheets are considered one of the most widely used end-user programming environments. Just as it is important for software to be free of bugs, spreadsheets need to be free of errors. This is important because in some cases, errors in spreadsheets can cost a financial entity thousands of dollars. In this work, we formulate a class of commonplace errors based on our manual inspection of real life spreadsheets, and further provide an analysis algorithm to detect these errors. We introduce ``reference counting'' as a simple yet effective algorithm to detect range errors. We finally demonstrate how reference counting can effectively point out erroneous cells in faulty spreadsheets.
@InProceedings{SPLASH Companion15p73,
author = {Nima Joharizadeh},
title = {Finding Bugs in Spreadsheets using Reference Counting},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {73--74},
doi = {},
year = {2015},
}
Viser: Providing Serializability in Hardware with Simplified Cache Coherence
Swarnendu Biswas
(Ohio State University, USA)
While existing architectures like x86 and SPARC provide strong hardware memory consistency models, such as TSO, programming language memory models are more relaxed. This divide nullifies the usefulness of providing strong hardware memory models, since languages and compilers provide a weaker guarantee. Moreover, current shared memory systems implement complex cache coherence protocols which add to the complexity.
This work proposes a microarchitecture, called Viser, that ensures strong semantics---serializability of synchronization-free regions (SFRs)---in the absence of region conflicts even for racy program executions. Given an execution, Viser either reports a serializability violation or guarantees SFR-serializability, in effect providing the same guarantees provided by languages such as C++ and Java for data-race-free programs only. Viser's design also allows for greatly simplifying existing cache coherence protocols, without requiring any assumptions about language-level properties such as data-race-freedom.
@InProceedings{SPLASH Companion15p75,
author = {Swarnendu Biswas},
title = {Viser: Providing Serializability in Hardware with Simplified Cache Coherence},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {75--76},
doi = {},
year = {2015},
}
Concurrency Control for Multithreaded Reactive Programming
Ragnar Mogk
(TU Darmstadt, Germany)
Reactive programming is a declarative style of defining applications which deal with continuous inputs of new data and events. Being declarative in nature, reactive programming allows the programmer to state the intent of the application, instead of specifying concrete execution behavior as needed in applications using the Observer design pattern. Declarative definitions not only improve code clarity, but also leave concrete execution behavior unspecified – the underlying runtime can freely change as long as the intended semantic is kept intact. We exploit this freedom to support concurrent propagation of concurrently admitted changes.
@InProceedings{SPLASH Companion15p77,
author = {Ragnar Mogk},
title = {Concurrency Control for Multithreaded Reactive Programming},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {77--78},
doi = {},
year = {2015},
}
Gradual Mode Types for Energy-Aware Programming
Anthony Canino
(SUNY Binghamton, USA)
Modeling energy related concepts as high level constructs that can be checked by a type system is challenging due to the dependency on runtime factors related to energy consumption. Pushing energy concepts such as energy mode types into a language helps less skilled programmers write energy-aware software without relying on lower level techniques that depend upon hardware. We develop a language that allows energy specific type checking to be done gradually with both static and dynamic checks. As a result we allow energy-aware programming that is both natural and flexible at the language level.
@InProceedings{SPLASH Companion15p79,
author = {Anthony Canino},
title = {Gradual Mode Types for Energy-Aware Programming},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {79--80},
doi = {},
year = {2015},
}
Race-Driven UI-Level Test Generation for JavaScript-Based Web Applications
Martin Billes
(TU Darmstadt, Germany)
Due to its asynchronous, event-driven nature, JavaScript, similar to concurrent programs, suffers from the problem of data races. Past research provides methods for automatically exploring a web application to generate a trace and uses an offline dynamic race detector to find data races in the application. However, the existing random exploration techniques fail to identify races that require complex interactions with the application. While more sophisticated approaches to explore websites exist, these are not targeted towards finding data races. We conduct a study of data race bugs in open source software that shows most data race bugs are related to AJAX requests. Motivated by these findings, we present an approach for UI-level test generation which explores a website with the goal to find additional data races.
@InProceedings{SPLASH Companion15p81,
author = {Martin Billes},
title = {Race-Driven UI-Level Test Generation for JavaScript-Based Web Applications},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {81--82},
doi = {},
year = {2015},
}
Contributions of the Under-Appreciated: Gender Bias in an Open-Source Ecology
Andrew Kofink
(North Carolina State University, USA)
Female software developers account for only a small portion of the total developer community. This inequality is caused by subtle beliefs and sometimes interactions between different genders and society, referred to as implicit biases and explicit behavior, respectively. In this study, I mined user contribution acceptance from a popular software collaboration service. The contributions of female developers were accepted into open-source projects with roughly equivalent success to those of males, partially discounting recent findings that explicit behavior accompanies implicit gender bias, while bolstering the claim that implicit bias is cultural, rather than as a result of innate differences.
@InProceedings{SPLASH Companion15p83,
author = {Andrew Kofink},
title = {Contributions of the Under-Appreciated: Gender Bias in an Open-Source Ecology},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {83--84},
doi = {},
year = {2015},
}
Safely Evolving Configurable Systems
Flávio Medeiros
(Federal University of Campina Grande, Brazil)
Developers use configuration options to tailor systems to different platforms. This configurability leads to exponential configuration spaces and traditional tools (e.g., gcc) check only one configuration at a time. As a result, developers introduce configuration-related issues (i.e., bad smells and faults) that appear only when we select certain configuration options. By interviewing 40 developers and performing a survey with 202 developers, we found that configuration- related issues are harder to detect and more critical than is- sues that appear in all configurations. We propose a strategy to detect configuration-related issues and a catalogue of refactorings to remove bad smells in preprocessor directives. We found 131 faults and 500 bad smells in 40 real-world configurable systems, including Apache and Libssh.
@InProceedings{SPLASH Companion15p85,
author = {Flávio Medeiros},
title = {Safely Evolving Configurable Systems},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {85--86},
doi = {},
year = {2015},
}
SIRe: An Efficient Snapshot Isolation-Based Memory Model for Detecting and Tolerating Region Conflicts
Minjia Zhang
(Ohio State University, USA)
A strong memory model, such as region serializability, helps programmers reason about programs in the granularity of synchronization free regions and allows compiler and hardware to more freely reorder accesses. However, providing region serializability usually is expensive in software or requires custom hardware.
We introduce a new approach to support a memory model that guarantees write-atomicity and a consistent snapshot view to reads in a synchronization free region by tolerating the majority region-conflicts caused by write-write and write-read conflicts and freezes the program state if a read-write conflict violates the memory model.
@InProceedings{SPLASH Companion15p87,
author = {Minjia Zhang},
title = {SIRe: An Efficient Snapshot Isolation-Based Memory Model for Detecting and Tolerating Region Conflicts},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {87--88},
doi = {},
year = {2015},
}
The Oprop Verification Tool: Object Propositions in Action
Ligia Nistor
(Carnegie Mellon University, USA)
We have recently introduced object propositions as a modular verification technique that combines abstract predicates and fractional permissions. The Oprop tool implements the theory of object propositions and verifies programs written in a simplified version of Java, augmented with the object propositions specifications. Our tool parses the input files and automatically translates them into the intermediate verification language Boogie, which is verified by the Boogie verifier. We present the details of our implementation, the lessons that we learned and a number of examples that we have verified using the Oprop tool.
@InProceedings{SPLASH Companion15p89,
author = {Ligia Nistor},
title = {The Oprop Verification Tool: Object Propositions in Action},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {89--90},
doi = {},
year = {2015},
}
proc time: 1.06