Resolving and Exploiting the k-CFA Paradox, Matthew Might, Yannis Smaragdakis, and David Van Horn. To appear in PLDI 2010.
Low-level program analysis is a fundamental problem, taking the shape of "flow analysis" in functional languages and "points-to" analysis in imperative and object-oriented (OO) languages. Despite the similarities, the vocabulary and results in the two communities remain largely distinct, with limited cross-understanding. One of the few links is Shivers's k-CFA work, which has advanced the concept of "context-sensitive analysis" and is widely known in both communities. Recent results, however, indicate that the relationship between the different incarnations of the analysis is not understood.
Van Horn and Mairson proved k-CFA for k ≥ 1 to be EXPTIME-complete, hence no polynomial algorithm exists. Yet there have been multiple polynomial formulations of context-sensitive points-to analyses in OO languages. Is functional k-CFA a profoundly different analysis from OO k-CFA? We resolve this paradox by showing that OO features conspire to make the exact same specification of k-CFA be polynomial-time: objects and closures are subtly different, in a way that interacts crucially with context-sensitivity. This leads to a significant practical result: by emulating the OO approximation, we derive a polynomial hierarchy of context-sensitive CFAs for functional programs, simultaneously achieving high precision and efficiency.
I learned that performance bounds on flow analysis were fascinating from earlier work by David van Horn and Harry Mairson, so it's good to see that this line of work is still being continued, and even better to see new algorithms come out of it.
Continuity Analysis of Programs, Swarat Chaudhuri, Sumit Galwani, and Roberto Lublinerman. POPL 2010.
We present an analysis to automatically determine if a program represents a continuous function, or equivalently, if infinitesimal changes to its inputs can only cause infinitesimal changes to its outputs. The analysis can be used to verify the robustness of programs whose inputs can have small amounts of error and uncertainty -- e.g., embedded controllers processing slightly unreliable sensor data, or handheld devices using slightly stale satellite data.
Continuity is a fundamental notion in mathematics. However, it is difficult to apply continuity proofs from real analysis to functions that are coded as imperative programs, especially when they use diverse data types and features such as assignments, branches, and loops. We associate data types with metric spaces as opposed to just sets of values, and continuity of typed programs is phrased in terms of these spaces. Our analysis reduces questions about continuity to verification conditions that do not refer to infinitesimal changes and can be discharged using off-the-shelf SMT solvers. Challenges arise in proving continuity of programs with branches and loops, as a small perturbation in the value of a variable often leads to divergent control-flow that can lead to large changes in values of variables. Our proof rules identify appropriate “synchronization points” between executions and their perturbed counterparts, and establish that values of certain variables converge back to the original results in spite of temporary divergence.
We prove our analysis sound with respect to the traditional epsilon-delta definition of continuity. We demonstrate the precision of our analysis by applying it to a range of classic algorithms, including algorithms for array sorting, shortest paths in graphs, minimum spanning trees, and combinatorial optimization. A prototype implementation based on the Z3 SMT-solver is also presented.
Another fun paper from POPL this year. I've seen metric spaces used to solve domain equations before, but the idea of actually considering a metric on the outputs was a new one to me.
Monads in Action, Andrzej Filinski, POPL 2010.
In functional programming, monadic characterizations of computational effects are normally understood denotationally: they describe how an effectful program can be systematically expanded or translated into a larger, pure program, which can then be evaluated according to an effect-free semantics. Any effect-specific operations expressible in the monad are also given purely functional definitions, but these definitions are only directly executable in the context of an already translated program. This approach thus takes an inherently Church-style view of effects: the nominal meaning of every effectful term in the program depends crucially on its type.
We present here a complementary, operational view of monadic effects, in which an effect definition directly induces an imperative behavior of the new operations expressible in the monad. This behavior is formalized as additional operational rules for only the new constructs; it does not require any structural changes to the evaluation judgment. Specifically, we give a small-step operational semantics of a prototypical functional language supporting programmer-definable, layered effects, and show how this semantics naturally supports reasoning by familiar syntactic techniques, such as showing soundness of a Curry-style effect-type system by the progress+preservation method.
The idea of monadic reflection was one I never felt I really understood properly until I read this paper, so now I'll have to go back and re-read some of his older papers on the subject.
While PHP deservedly gets a terrible rep around programming language folks, this is still an interesting announcement: HipHop compiles PHP down to C++ and gets about a 2x speedup. HipHop will be released as open source, and is currently in production use, serving 90% of Facebook's traffic. It makes me wish Facebook used Python: a large-scale deployment like this would be a great boon to the PyPy project.
Delimited Control in OCaml, Abstractly and Concretely, System Description
We describe the first implementation of multi-prompt delimited control operators in OCaml that is direct in that it captures only the needed part of the control stack. The implementation is a library that requires no changes to the OCaml compiler or run-time, so it is perfectly compatible with existing OCaml source code and byte-code. The library has been in fruitful practical use for four years.
We present the library as an implementation of an abstract machine derived by elaborating the definitional machine. The abstract view lets us distill a minimalistic API, scAPI, sufficient for implementing multi-prompt delimited control. We argue that a language system that supports exception and stack-overflow handling supports scAPI. Our library illustrates how to use scAPI to implement multi-prompt delimited control in a typed language. The approach is general and can be used to add multi-prompt delimited control to other existing language systems.
Oleg was kind enough to send me an e-mail letting me know of this paper's existence (it appears not yet to be linked from the "Computation" page under which it is stored) and to include me in the acknowledgements. Since the paper in its current form has been accepted for publication, he indicated that it can be made more widely available, so here it is. In typical Oleg fashion, it offers insights at both the theoretical and implementation levels.
Leo Meyerovich recently started a thread on LtU asking about Historical or sociological studies of programming language evolution?. I've been meaning to post a paper on this topic to LtU for awhile now, but simply cherrypicking for the opportune time to fit it into forum discussion. With Leo's question at hand, I give you an interesting paper that models language evolution, by artificial intelligence researcher Luc Steels. Steels has spent over 10 years researching this area, and his recent paper, The Recruitment Theory of Language Origins, summarizes one of his models for dealing with language evolution:
The recruitment theory of language origins argues that language users recruit and try out different strategies for solving the task of communication and retain those that maximise communicative success and cognitive economy. Each strategy requires specific cognitive neural mechanisms, which in themselves serve a wide range of purposes and therefore may have evolved or could be learned independently of language. The application of a strategy has an impact on the properties of the emergent language and this fixates the use of the strategy in the population. Although neurological evidence can be used to show that certain cognitive neural mechanisms are common to linguistic and non-linguistic tasks, this only shows that recruitment has happened, not why. To show the latter, we need models demonstrating that the recruitment of a particular strategy and hence the mechanisms to carry out this strategy lead to a better communication system. This paper gives concrete examples how such models can be built and shows the kinds of results that can be expected from them.
I owe Martin Odersky and his team at EPFL an apology: as you can see, I'm posting this rather dramatically late, as the deadline for submission has already passed. Nevertheless, hopefully the notice of the event itself is still worthwhile.
Sheepishly,
Paul
The First Scala Workshop
========================
Call for Papers
---------------
Scala is a general purpose programming language designed to express
common programming patterns in a concise, elegant, and type-safe
way. It smoothly integrates features of object-oriented and
functional languages.
This workshop is a forum for researchers and practitioners to share
new ideas and results of interest to the Scala community. The first
workshop will be held at EPFL in Lausanne, Switzerland, on Thursday
15 April 2010, co-located with Scala Days 2010 (15-16 April).
We seek papers on topics related to Scala, including (but not
limited to):
1. Language design and implementation -- language extensions,
optimization, and performance evaluation.
2. Library design and implementation patterns for extending Scala --
embedded domain-specific languages, combining language features,
generic and meta-programming.
3.Formal techniques for Scala-like programs -- formalizations of the
language, type system, and semantics, formalizing proposed language
extensions and variants, dependent object types, type and effect
systems.
4. Concurrent and distributed programming -- libraries, frameworks,
language extensions, programming paradigms: (Actors, STM, ...),
performance evaluation, experimental results.
5. Safety and reliability -- pluggable type systems, contracts,
static analysis and verification, runtime monitoring.
6. Tools -- development environments, debuggers, refactoring
tools, testing frameworks.
7. Case studies, experience reports, and pearls
Important Dates
---------------
Submission: Friday, Jan 15, 2010 (24:00 in Apia, Samoa)
Notification: Monday, Feb 15, 2010
Final revision: Monday, Mar 15, 2010
Workshop: Thursday, Apr 15, 2010
Submission Guidelines
---------------------
Submitted papers should describe new ideas, experimental results, or
projects related to Scala. In order to encourage lively discussion,
submitted papers may describe work in progress. All papers will be
judged on a combination of correctness, significance, novelty,
clarity, and interest to the community.
Submissions must be in English and at most 12 pages total length in
the standard ACM SIGPLAN two-column conference format (10pt).
No formal proceedings will be published, but there will be a webpage
linking to all accepted papers. The workshop also welcomes short papers.
Submission instructions will be published at:
http://www.scala-lang.org/days2010
Program Committee
-----------------
Ian Clarke, Uprizer Labs
William Cook, UT Austin
Adriaan Moors, KU Leuven
Martin Odersky, EPFL (chair)
Kunle Olukotun, Stanford University
David Pollak, Liftweb
Lex Spoon, Google
Picture or screenshot driven programming from the MIT.
From the Sikuli project page:
Sikuli is a visual technology to search and automate graphical user interfaces (GUI) using images (screenshots). The first release of Sikuli contains Sikuli Script, a visual scripting API for Jython, and Sikuli IDE, an integrated development environment for writing visual scripts with screenshots easily.
I have done some work recently on the theory of aliasing, which I believe provides the key to the frame problem and more generally to proving O-O programs (although these applications remain to be better explained and explored further).
I was struck by the simplicity and generality of the laws uncovered in the process.
A blog entry at bertrandmeyer.com presents the basics. It includes a link to the draft paper, and also to a downloadable version of the implementation (currently a Windows executable, the source will be released later), which makes it possible to test all the examples of the paper.
-- Bertrand Meyer
|
