Arrival and Coffee: 9:30 - 10:00
Session 1: 10:00 - 10:45
Jeffery Mark Siskind (Purdue University)
Backpropagation Through Functional Programs
How to do Reverse-Mode AD Correctly in a Functional Framework
Break: 10:45 - 11:00
Session 2: 11:00 - 12:30
Christopher League (Long Island University)
MetaOCaml Server Pages:
Web Publishing as Staged Computation
Xinyu Feng (Yale University)
Modular Verification of Concurrent Assembly Code with Dynamic Thread
Creation and Termination
Lunch: 12:30 - 1:50
Business meeting: 1:50 - 2:00
Session 3: 2:00 - 3:30
Liqiang Wang (State University of New York at Stony Brook)
Static Analysis of Atomicity for Programs with Non-Blocking
Synchronization
Rahul Agarwal (State University of New York at Stony Brook)
Optimized Run-Time Race Detection And Atomicity
Checking Using Partial Discovered Types
Abstract: We show how reverse-mode AD (automatic differentiation)---a generalized gradient-calculation operator---can be incorporated as a first-class function in a functional-programming language. An important property of AD transformations is that they preserve certain complexity properties. Here, this property is that the reverse phase of the reverse-mode transform of a function has the same time complexity (up to a small constant factor) as the original untransformed function. The main technical difficulty to be faced is that reverse-mode AD must convert fanout (multiple use of a variable) in the untransformed code into addition in the reverse phase of the transformed code. We address this by expressing all straight-line code segments in A-normal form, which makes fanout lexically apparent. Our formulation generalizes reverse-mode AD to apply to arbitrary higher-order functions, while preserving its desirable complexity properties.
Joint work with Barak A. Pearlmutter
Abstract: Modern dynamic web services are really computer programs. Some parts of these programs run off-line, others run server-side on each request, and still others run within the browser. In other words, web publishing is staged computation, either for better performance, or because certain resources are available in one stage but not another. Unfortunately, the various web programming languages make it difficult to spread computation over more than one stage. This is a tremendous opportunity for multi-stage languages in general, and for MetaOCaml in particular.
We present the design of MetaOCaml Server Pages. Unlike other languages in its genre, the embedded MetaOCaml code blocks may be annotated with staging information, so that the programmer may safely and precisely control which computation occurs in which stage. A prototype web server, written in OCaml, supports web sites with both static and dynamic content. We provide several sample programs and demonstrate the performance gains won using multi-stage programming.
Abstract: Proof-carrying code (PCC) is a general framework that can, in principle, verify safety properties of arbitrary machine-language programs. Existing PCC systems and typed assembly languages, however, can only handle sequential programs. This severely limits their applicability since many real-world systems use some form of concurrency in their core software. Recently Yu and Shao proposed a logic-based ``type'' system for verifying concurrent assembly programs. Their thread model, however, is rather restrictive in that no threads can be created or terminated dynamically and no sharing of code is allowed between threads. In this paper, we present a new formal framework for verifying general multi-threaded assembly code with unbounded dynamic thread creation and termination as well as sharing of code between threads. We adapt and generalize the rely-guarantee methodology to the assembly level and show how to specify the semantics of thread ``fork'' with argument passing. In particular, we allow threads to have different assumptions and guarantees at different stages of their lifetime so they can coexist with the dynamically changing thread environment. Our work provides a foundation for certifying realistic multi-threaded programs and makes an important advance toward generating proof-carrying concurrent code.
This is joint work with Prof. Zhong Shao and the paper is accepted in this year's ICFP (a preprint version of the paper is available in the FLINT web page: http://flint.cs.yale.edu/publications/).
Abstract: In concurrent programming, non-blocking synchronization is very efficient but difficult to design correctly. This paper presents a static analysis to show that code blocks are atomic, i.e., that every execution of the program is equivalent to one in which those code blocks execute without interruption by other threads. Our analysis determines commutativity of operations based primarily on how synchronization primitives (including locks, load-linked, store-conditional, and compare-and-swap) are used. A reduction theorem states that certain patterns of commutativity imply atomicity. Atomicity is itself an important correctness requirement for many concurrent programs. Furthermore, an atomic code block can be treated as a single transition during subsequent analysis of the program; this can greatly improve the efficiency of the subsequent analysis. We demonstrate the effectiveness of our approach on several concurrent non-blocking programs.
This is the joint work with Scott D. Stoller.
The original paper appeared in Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP 2005). It is available here: PPoPP05-nonblocking.pdf.
Abstract:Concurrent programs are notorious for containing errors that are difficult to reproduce and diagnose. Two common kinds of concurrency errors are data races and atomicity violations (informally, atomicity means that executing methods concurrently is equivalent to executing them serially). Several static and dynamic (run-time) analysis techniques exist to detect potential races and atomicity violations. Run-time checking may miss errors in unexecuted code and incurs significant run-time overhead. On the other hand, run-time checking generally produces fewer false alarms than static analysis; this is a significant practical advantage, since diagnosing all of the warnings from static analysis of large codebases may be prohibitively expensive. This paper explores the use of static analysis to significantly decrease the overhead of run-time checking. Our approach is based on a type system for analyzing data races and atomicity. A type discovery algorithm is used to obtain types for as much of the program as possible (complete type inference for this type system is NP-hard, and parts of the program might be untypable). Warnings from the typechecker are used to identify parts of the program from which run-time checking can safely be omitted. The approach is completely automatic, scalable to very large programs, and significantly reduces the overhead of run-time checking for data races and atomicity violations.
This paper was accepted at ASE'05, and is joint work with Amit Sasturkar, Liqiang Wang and Scott Stoller. A preliminary version of the paper is available at: www.cs.sunysb.edu/~ragarwal