Theory

Concurrent Pattern Calculus

Concurrent Pattern Calculus by Thomas Given-Wilson, Daniele Gorla, and Barry Jay:

Concurrent pattern calculus drives interaction between processes by comparing data structures, just as sequential pattern calculus drives computation. By generalising from pattern matching to pattern unification , interaction becomes symmetrical, with information flowing in both directions. This provides a natural language for describing any form of exchange or trade. Many popular process calculi can be encoded in concurrent pattern calculi.

Barry Jay's Pattern Calculus has been discussed a few times here before. I've always been impressed with the pattern calculus' expressive power for computing over arbitrary structure. The pattern calculus supports new forms of polymorphism, which he termed "path polymorphism" and "pattern polymorphism", which are difficult to provide in other calculi. The closest I can think of would be a compiler-provided generalized fold over any user-defined structure.

This work extends the pattern calculus to the concurrent setting by adding constructs for parallel composition, name restriction and replication, and argues convincingly for its greater expressiveness as compared to other concurrent calculi. He addresses some of the obvious concerns for symmetric information flow of the unification operation.

Parametric Prediction of Heap Memory Requirements

Parametric Prediction of Heap Memory Requirements, by Victor Braberman, Federico Fernandez, Diego Garbervetsky, Sergio Yovine:

This work presents a technique to compute symbolic polynomial approximations of the amount of dynamic memory required to safely execute a method without running out of memory, for Java-like imperative programs. We consider object allocations and deallocations made by the method and the methods it transitively calls. More precisely, given an initial configuration of the stack and the heap, the peak memory consumption is the maximum space occupied by newly created objects in all states along a run from it. We over-approximate the peak memory consumption using a scoped-memory management where objects are organized in regions associated with the lifetime of methods. We model the problem of computing the maximum memory occupied by any region configuration as a parametric polynomial optimization problem over a polyhedral domain and resort to Bernstein basis to solve it. We apply the developed tool to several benchmarks.

We've briefly discussed analyses to predict heap usage here on LtU, but I can't seem to find them. Anyone with a reference handy, please post in the comments!

Automatic Staged Compilation

Automatic Staged Compilation, doctoral dissertation of Matthai Philipose:

[...] The past few years have seen the emergence of staged optimization, which produces run-time optimizations that often have much lower run-time overhead than traditional optimizers, yet do not sacrifice any of their functionality. The key to the technique is a method, called staging, to transfer optimization overhead to static compile time from run time. Unfortunately, developing staged variants of individual optimizations has been highly specialized, labor-intensive work; staging pipelines of optimizations even more so.

This dissertation presents a system called the Staged Compilation Framework (SCF), which automatically stages entire pipelines of compiler optimizations at arguably little additional engineering cost beyond building the slower traditional version of the pipeline. SCF harnesses two powerful but traditionally difficult-to-use techniques, partial evaluation and dead-store elimination, to achieve staging. An implementation of SCF shows that staged compilation can speed up pipelines of classical compiler optimizations by up to an order of magnitude, and more commonly by a factor of 4.5 to 5.

I haven't read through it all yet, but after a cursory skim it certainly looks interesting.

Yacc is dead

In Yacc is dead (2010) Matthew Might and David Darais of the University of Utah, Salt Lake City...

present two novel approaches to parsing context-free languages. The first approach is based on an extension of Brzozowski’s derivative from regular expressions to context-free grammars. The second approach is based on a generalization of the derivative to parser combinators. The payoff of these techniques is a small (less than 250 lines of code), easy-to-implement parsing library capable of parsing arbitrary context-free grammars into lazy parse forests. Implementations for both Scala and Haskell are provided. Preliminary experiments with S-Expressions parsed millions of tokens per second, which suggests this technique is efficient enough for use in practice.

It seems every problem in computer science can be solved with either one more level of indirection or a derivative.

Conservative Logic

Edward Fredkin and Tommoasso Toffoli from the MIT Labratory for Computer Science present Conservative Logic...

a comprehensive model of computation which explicitly reflects a number of fundamental principles of physics, such as the reversibility of the dynamical laws and the conservation of certain additive quantities (among which energy plays a distinguished role). Because it more closely mirrors physics than traditional models of computation, conservative logic is in a better position to provide indications concerning the realization of high-performance computing systems, i.e., of systems that make very efficient use of the "computing resources" actually offered by nature. In particular, conservative logic shows that it is ideally possible to build sequential circuits with zero internal power dissipation. After establishing a general framework, we discuss two specific models of computation. The first uses binary variables and is the conservative-logic counterpart of switching theory; this model proves that universal computing capabilities are compatible with the reversibility and conservation constraints. The second model, which is a refinement of the first, constitutes a substantial breakthrough in establishing a correspondence between computation and physics. In fact, this model is based on elastic collisions of identical "balls," and thus is formally identical with the atomic model that underlies the (classical) kinetic theory of perfect gases. Quite literally, the functional behavior of a general-purpose digital computer can be reproduced by a perfect gas placed in a suitably shaped container and given appropriate initial conditions.

This paper has a small discussion in a forum thread mostly saying the paper should be on the front page.

Eff - Language of the Future

This is just a series of blog posts so far, as far as I can tell. But Andrej Bauer's work has been mentioned here many times, I am finding these posts extremely interesting, and I'm sure I will not be alone. So without further ado...

Programming With Effects. Andrej Bauer and Matija Pretnar.

I just returned from Paris where I was visiting the INRIA πr² team. It was a great visit, everyone was very hospitable, the food was great, and the weather was nice. I spoke at their seminar where I presented a new programming language eff which is based on the idea that computational effects are algebras. The language has been designed and implemented jointly by Matija Pretnar and myself. Eff is far from being finished, but I think it is ready to be shown to the world. What follows is an extended transcript of the talk I gave in Paris. It is divided into two posts. The present one reviews the basic theory of algebras for a signature and how they are related to computational effects. The impatient readers can skip ahead to the second part, which is about the programming language.

Formal Compiler Implementation in a Logical Framework

Hickey, Jason and Nogin, Aleksey and Granicz, Adam and Aydemir, Brian (2003) Formal Compiler Implementation in a Logical Framework. Technical Report. California Institute of Technology.

The task of designing and implementing a compiler can be a difficult and error-prone process. In this paper, we present a new approach based on the use of higher-order abstract syntax and term rewriting in a logical framework. All program transformations, from parsing to code generation, are cleanly isolated and specified as term rewrites. This has several advantages. The correctness of the compiler depends solely on a small set of rewrite rules that are written in the language of formal mathematics. In addition, the logical framework guarantees the preservation of scoping, and it automates many frequently-occurring tasks including substitution and rewriting strategies. As we show, compiler development in a logical framework can be easier than in a general-purpose language like ML, in part because of automation, and also because the framework provides extensive support for examination, validation, and debugging of the compiler transformations. The paper is organized around a case study, using the MetaPRL logical framework to compile an ML-like language to Intel x86 assembly. We also present a scoped formalization of x86 assembly in which all registers are immutable.

I don't understand the details of this paper, but the general approach of using rewriting for compilation (including passes such as closure conversion) is very interesting in itself.

(Edit: As a bonus, the paper is derived from the literate MetaPRL sources.)

(Edit: Oleg's applicative-order term rewriting system for code generation shows how simpler rewriting systems can be used in the context of compilation.)

Tropical Semirings

Tropical Semirings, Jean-Éric Pin. Idempotency 1994.

It is a well-known fact that the boolean calculus is one of the mathematical foundations of electronic computers. This explains the important role of the boolean semiring in computer science. The aim of this paper is to present other semirings that occur in theoretical computer science. These semirings were baptized tropical semirings by Dominique Perrin in honour of the pioneering work of our brazilian colleague and friend Imre Simon, but are also commonly known as (min, +)-semirings.

In the previous post, Ohad Kammar asked for some more examples of why we should care about adjunctions, which reminded me of one of my favorite examples. You can understand solving many optimization problems as looking for a Galois connection between your problem and the tropical semiring. (Galois connections in general are one of the sources of the program derivation superpowers of the Squiggolists. So if you want to prove programs like Shin Cheng-Mu does, it's worth understanding!)

The Structure of Authority: Why security is not a separable concern

The Structure of Authority: Why security is not a separable concern, by Mark S. Miller, Bill Tulloh, and Jonathan Shapiro:

Common programming practice grants excess authority for the sake of functionality; programming principles require least authority for the sake of security. If we practice our principles, we could have both security and functionality. Treating security as a separate concern has not succeeded in bridging the gap between principle and practice, because it operates without knowledge of what constitutes least authority. Only when requests are made -- whether by humans acting through a user interface, or by one object invoking another -- can we determine how much authority is adequate. Without this knowledge, we must provide programs with enough authority to do anything they might be requested to do.

We examine the practice of least authority at four major layers of abstraction -- from humans in an organization down to individual objects within a programming language. We explain the special role of object-capability languages -- such as E or the proposed Oz-E -- in supporting practical least authority.

An important overview of why security properties cannot be an after-thought for any platform, languages and operating systems included. To this end, the paper covers security properties at various granularities from desktop down to object-level granularity, and how object-capabilities provide security properties that are compositional, and permit safely composing mutually suspicious programs.

A recent LtU discussion on achieving security by built-in object-capabilities vs. building security frameworks as libraries reminded me of this paper. Ultimately, the library approach can work assuming side-effects are properly controlled via some mechanism, ie. effect types or monads, but any solution should conform to object capability principles to maintain safe composition.

An example of a capability-secure legacy/library approach is Plash (Principle of Least Authority SHell), which provides object-specific file system name spaces. Any library interface to the file system should mimic this file system virtualization, which effectively pushes side-effect control down to OS-level objects, and which is essential to safely composing mutually suspicious programs that access the file system.

A Formal System For Euclid's Elements

A Formal System For Euclid's Elements, Jeremy Avigad, Edward Dean, and John Mumma. Review of Symbolic Logic, Vol. 2, No. 4, 2009.

Abstract. We present a formal system, E, which provides a faithful model of the proofs in Euclid’s Elements, including the use of diagrammatic reasoning.

Diagrammatic languages are a perennial favorite discussion topic here, and Euclid's proofs constitute one of the oldest diagrammatic languages around. And yet for hundreds of years (at least since Leibniz) people have argued about whether or not the diagrams are really part of a formal system of reasoning, or whether they are simply visual aids hanging on the side of the true proof. The latter position is the one that Hilbert and Tarski took as well when they gave formal axiomatic systems for geometry.

But was this necessary, or just a contingent fact of the logical machinery available to them? Avigad and his coauthors show the former point of view also works, and that you can do it with very basic proof theory (there's little here unfamiliar to anyone who has read Pierce's book). Yet it sheds a lot of light on how the diagrams in the Elements work, in part because of their very careful analysis of how to read the diagrams -- that is, what conclusion a diagram really licenses you to draw, and which ones are accidents of the specific figure on the page. How they consider these issues is a good model for anyone designing their own visual programming languages.

XML feed