Programming Languages and Systems

A fundamental belief underlying forty years of programming languages research, aptly captured by the slogan “Well-typed programs can’t go wrong”, is that programs augmented with machine-checked annotations are more likely to be free of bugs. But of course, real programs do wrong and programmers are voting with their feet. Dynamic languages such as Ruby, Python, Lua, JavaScript and R are unencumbered by redundant type annotations and are increasingly popular. JavaScript, the lingua franca of the web, is moving to the server with the success of Node.js. R, another dynamic language, is being used in statistics, biology and finance for data analysis and visualization. Not only are these languages devoid of types, but they utterly lack any static structure that could be used for program verification. This talk will draw examples from recent results on JavaScript and R to illustrate the extent of the problem and propose some directions for research. R. Jhala and A. Igarashi (Eds.): APLAS 2012, LNCS 7705, p. 1, 2012. c © Springer-Verlag Berlin Heidelberg 2012 JATO: Native Code Atomicity for Java Siliang Li, Yu David Liu, and Gang Tan 1 Department of Computer Science & Engineering, Lehigh University 2 Department of Computer Science, SUNY Binghamton Abstract. Atomicity enforcement in a multi-threaded application can be critical to the application’s safety. In this paper, we take the challenge of enforcing atomicity in a multilingual application, which is developed in multiple programming languages. Specifically, we describe the design and implementation of JATO, which enforces the atomicity of a native method when a Java application invokes the native method through the Java Native Interface (JNI). JATO relies on a constraint-based system, which generates constraints from both Java and native code based on how Java objects are accessed by threads. Constraints are then solved to infer a set of Java objects that need to be locked in native methods to enforce the atomicity of the native method invocation. We also propose a number of optimizations that soundly improve the performance. Evaluation through JATO’s prototype implementation demonstrates it enforces native-method atomicity with reasonable run-time overhead. Atomicity enforcement in a multi-threaded application can be critical to the application’s safety. In this paper, we take the challenge of enforcing atomicity in a multilingual application, which is developed in multiple programming languages. Specifically, we describe the design and implementation of JATO, which enforces the atomicity of a native method when a Java application invokes the native method through the Java Native Interface (JNI). JATO relies on a constraint-based system, which generates constraints from both Java and native code based on how Java objects are accessed by threads. Constraints are then solved to infer a set of Java objects that need to be locked in native methods to enforce the atomicity of the native method invocation. We also propose a number of optimizations that soundly improve the performance. Evaluation through JATO’s prototype implementation demonstrates it enforces native-method atomicity with reasonable run-time overhead.