Teaching & Learning
Is Transactional Programming Actually Easier?, WDDD '09, Christopher J. Rossbach, Owen S. Hofmann, and Emmett Witchel.
Chip multi-processors (CMPs) have become ubiquitous, while tools that ease concurrent programming have not. The promise of increased performance for all applications through ever more parallel hardware requires good tools for concurrent programming, especially for average programmers. Transactional memory (TM) has enjoyed recent interest as a tool that can help programmers program concurrently.
The TM research community claims that programming with transactional memory is easier than alternatives (like locks), but evidence is scant. In this paper, we describe a user-study in which 147 undergraduate students in an operating systems course implemented the same programs using coarse and fine-grain locks, monitors, and transactions. We surveyed the students after the assignment, and examined their code to determine the types and frequency of programming errors for each synchronization technique. Inexperienced programmers found baroque syntax a barrier to entry for transactional programming. On average, subjective evaluation showed that students found transactions harder to use than coarse-grain locks, but slightly easier to use than fine-grained locks. Detailed examination of synchronization errors in the studentsâ€™ code tells a rather different story. Overwhelmingly, the number and types of programming errors the students made was much lower for transactions than for locks. On a similar programming problem, over 70% of students made errors with fine-grained locking, while less than 10% made errors with transactions.
I've recently discovered the Workshop on Duplicating, Deconstructing, and Debunking (WDDD) and have found a handful of neat papers, and this one seemed especially relevant to LtU.
[Edit: Apparently, there is a PPoPP'10 version of this paper with 237 undergraduate students.]
Also, previously on LtU:
Transactional Memory versus Locks - A Comparative Case Study
Despite the fact Tommy McGuire's post mentions Dr. Victor Pankratius's talk was at UT-Austin and the authors of this WDDD'09 paper represent UT-Austin, these are two independent case studies with different programming assignments. The difference in assignments is interesting because it may indicate some statistical noise associated with problem domain complexity (as perceived by the test subjects) and could account for differences between the two studies.
Everyone always likes to talk about usability in programming languages without trying to do it. Some claim it can't even be done, despite the fact Horning and Gannon did work on the subject 3+ decades ago, assessing how one can Language Design to Enhance Program Reliability. This gives a glimpse both on (a) why it is hard (b) how you can still try to do usability testing, rather than determine the truthiness of a language design decision.
Matthew Might, "Abstract interpreters for free", Static Analysis Symposium 2010 (SAS 2010).
...we present a two-step method to convert a small-step concrete semantics into a family of sound, computable abstract interpretations. The first step re-factors the concrete state-space to eliminate recursive structure; this refactoring of the state-space simultaneously determines a store-passing-style transformation on the underlying concrete semantics. The second step uses inference rules to generate an abstract state-space and a Galois connection simultaneously. The Galois connection allows the calculation of the â€œoptimalâ€ abstract interpretation. The two-step process is unambiguous, but nondeterministic: at each step, analysis designers face choices. Some of these choices ultimately influence properties such as flow-, field- and context-sensitivity. Thus, under the method, we can give the emergence of these properties a graph-theoretic characterization.
The work in this paper provides some context for known static analysis techniques like k-CFA, and also opens up some interesting new directions for static analysis development. Also, as Matt points out, there are some pedagogical benefits to having a systematic process for getting from semantics to abstract interpretation.
Why Undergraduates Should Learn the Principles of Programming Languages
The linked document is the first public release of a document discussing the value of programming languages principles for undergraduate CS majors. The intended audience is computer scientists who are not specialists in programming languages. Please leave comments on how well you believe it meets its goals and with suggestions for improvements.
Abstract: Undergraduate students obtain important knowledge and skills by studying the pragmatics of programming in multiple languages and the principles underlying programming language design and implementation. These topics strengthen students' grasp of the power of computation, help students choose the most appropriate programming model and language for a given problem, and improve their design skills. Understanding programming languages thus helps students in ways vital to many career paths and interests.
It would be nice if people interested in this as much as Kim Bruce could actively post such stuff to LtU as contributing editors, hint hint professors...
Edit: In case Kim Bruce is listening, I found this link today via Hacker News posting. There are some comments there, too.
Maxine VM is an open source meta-circular JVM from Sun.
Maxine is a VM designed for and written in the Java(TM) Programming Language with an emphasis on leveraging meta-circularity, componentized design, and code reuse to achieve flexibility, configurability, and productivity for academic and industrial virtual machine researchers.
The Maxine Inspector [5min, YouTube] seems pretty neat! Bringing VM research to the masses :)
A longer presentation by Bernd Mathiske at the JVM Language Summit 2008 provides a good introduction.
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.
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
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
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
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
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
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:
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
Certified Programming With Dependent Types
From the introduction:
We would all like to have programs check that our programs are correct. Due in no small part to some bold but unfulfilled promises in the history of computer science, today most people who write software, practitioners and academics alike, assume that the costs of formal program verification outweigh the benefits. The purpose of this book is to convince you that the technology of program verification is mature enough today that it makes sense to use it in a support role in many kinds of research projects in computer science. Beyond the convincing, I also want to provide a handbook on practical engineering of certified programs with the Coq proof assistant.
This is the best Coq tutorial that I know of, partially for being comprehensive, and partially for taking a very different tack than most with Adam's emphasis on proof automation using Coq's Ltac tactic language. It provides an invaluable education toward understanding what's going on either in LambdaTamer or Ynot, both of which are important projects in their own rights.
Please note that Adam is explicitly requesting feedback on this work.
Mitchel Resnick, John Maloney, AndreÌs Monroy HernaÌndez, Natalie Rusk, Evelyn Eastmond, Karen Brennan, Amon Millner, Eric Rosenbaum, Jay Silver, Brian Silverman, Yasmin Kafai, Scratch: Programming for All, Communications of the ACM, vol. 52, no. 11, November 2009.
When Moshe Vardi, Editor-in-Chief of CACM, invited us to submit an article about
Scratch, he shared the story of how he learned about Scratch:
A couple of days ago, a colleague of mine (CS faculty) told me how she tried to
get her 10-year-old daughter interested in programming, and the only thing that
appealed to her daughter (hugely) was Scratch.
Thatâ€™s what we were hoping for when we set out to develop Scratch six years ago. We
wanted to develop an approach to programming that would appeal to people who hadnâ€™t
previously imagined themselves as programmers. We wanted to make it easy for
everyone, of all ages, backgrounds, and interests, to program their own interactive stories,
games, animations, and simulations â€“ and to share their creations with one another.
Scratch is the cover story of the November 2009 issue of CACM. The goal of Scratch is to get kids programming so that they become more fluent in information technology, and develop "computational thinking" skills. Scratch is a graphical language based on a collection of â€œprogramming blocksâ€ that children snap together like Lego blocks to create programs. The programs themselves appear to be imperative in nature (at least based on the samples in the CACM article). Programs can be made concurrent by creating multiple stacks of blocks, and the authors claim that their goal is to make concurrent execution as intuitive as parallel execution.
Scratch was previously mentioned on LtU here.
A survey about state of the art C compiler optimization tricks, Felix von Leitner, Linux Kongress 2009.
The introduction and the conclusion is quite well put:
- If you do an optimization, test it on real world data.
- If itâ€™s not drastically faster but makes the code less readable: undo it.
That's certainly something that I agree with 110%. And really, that's why a good compilers course is so important, even if the vast majority of students never write a compiler outside of class.
Safe Garbage Collection = Regions + Intensional Type Analysis, by Daniel C. Wang and Andrew W. Appel:
We present a technique to implement type-safe garbage collectors by combining existing type systems used for compiling type-safe languages. We adapt the type systems used in region inference  and intensional type analysis  to construct a safe stop-and-copy garbage collector for higher-order polymorphic languages. Rather than using region inference as the primary method of storage management, we show how it can be used to implement a garbage collector which is provably safe. We also introduce a new region calculus with non-nested object lifetimes which is signiï¬cantly simpler than previous calculi. Our approach also formalizes more of the interface between garbage collectors and code generators. The efï¬ciency of our safe collectors are algorithmically competitive with unsafe collectors.
I'm surprised this region calculus hasn't received more attention or follow-up discussion in subsequent papers. It seems eminently practical, as it replaces the more complicated alias analyses required in other region calculi, with garbage collection of region handles; seems like a huge improvement over general GC, assuming region inference is sufficiently precise.
Verified Programming in Guru is a tutorial introduction to Guru:
GURU is a pure functional programming language, which is similar in some ways to Caml and Haskell. But GURU also contains a language for writing formal proofs demonstrating the properties of programs. So there are really two languages: the language of programs, and the language of proofs.
In comparison to Coq:
GURU is inspired largely by the COQ theorem prover, used for formalized mathematics and theoretical computer science, as well as program verification. Like COQ, GURU has syntax for both proofs and programs, and supports dependent types. GURU does not have as complex forms of polymorphism and dependent types as COQ does. But GURU supports some features that are difficult or impossible for COQ to support, which are useful for practical program verification. In COQ, the compiler must be able to confirm that all programs are uniformly terminating: they must terminate on all possible inputs. We know from basic recursion theory or theoretical computer science that this means there are some programs which really do terminate on all inputs that the compiler will not be able to confirm do so. Furthermore, some programs, like web servers or operating systems, are not intended to terminate. So that is a significant limitation. Other features GURU has that COQ lacks include support for functional modeling of non-functional constructs like destructive updates of data structures and arrays; and better support for proving properties of dependently typed functions.
The tutorial is worth a read to anybody new to this style of programming as it is one of the most gentle introductions to dependent types and automated program verification that I've seen.