Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, Francesco Zappa Nardelli. Common Compiler Optimisations are Invalid in the C11 Memory Model, and what we can do about it. In Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015.pdf ]
We show that the weak memory model introduced by the 2011 C and C++ standards is flawed because it does not permit many common source-to-source program transformations (such as expression linearisation and ``roach motel'' reorderings) that modern compilers (such as gcc and LLVM) perform and that are deemed to be correct. As such it cannot be used to define the semantics of intermediate languages of compilers, as, for instance, LLVM aimed to. We consider a number of possible local fixes, some strengthening and some weakening the model. We evaluate the proposed fixes by determining which program transformations are valid with respect to each of the patched models. We provide formal Coq proofs of their correctness or counterexamples as appropriate.

Thibaut Balabonski, François Pottier, and Jonathan Protzenko. Type soundness and race freedom for mezzo. In Functional and Logic Programming - 12th International Symposium, FLOPS 2014, Kanazawa, Japan, June 4-6, 2014. Proceedings, pages 253--269, 2014. [ bib | DOI | .pdf ]
The programming language Mezzo is equipped with a rich type system that controls aliasing and access to mutable memory. We incorporate shared-memory concurrency into Mezzo and present a modular formalization of its core type system, in the form of a concurrent λ-calculus, which we extend with references and locks. We prove that well-typed programs do not go wrong and are data-race free. Our definitions and proofs are machine-checked.

Thibaut Balabonski. Weak optimality, and the meaning of sharing. In ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013, pages 263--274, 2013. [ bib | DOI | .pdf ]
In this paper we investigate laziness and optimal evaluation strategies for functional programming languages. We consider the weak lambda-calculus as a basis of functional programming languages, and we adapt to this setting the concepts of optimal reductions that were defined for the full lambda-calculus. We prove that the usual implementation of call-by-need using sharing is optimal, that is, normalizing any lambda-term with call-by-need requires exactly the same number of reduction steps as the shortest reduction sequence in the weak lambda-calculus without sharing. Furthermore, we prove that optimal reduction sequences without sharing are not computable. Hence sharing is the only computable means to reach weak optimality.

Keywords: computability, evaluation strategies, laziness, optimality, sharing, weak reduction
Thibaut Balabonski. A unified approach to fully lazy sharing. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, pages 469--480, 2012. [ bib | DOI | .pdf ]
We give an axiomatic presentation of sharing-via-labelling for weak lambda-calculi, that makes it possible to formally compare many different approaches to fully lazy sharing, and obtain two important results. We prove that the known implementations of full laziness are all equivalent in terms of the number of beta-reductions performed, although they behave differently regarding the duplication of terms. We establish a link between the optimality theories of weak lambda-calculi and first-order rewriting systems by expressing fully lazy lambda-lifting in our framework, thus emphasizing the first-order essence of weak reduction.

Keywords: evaluation strategies, full laziness, labelling, lambda-calculus, lambda-lifting, optimality, rewriting, sharing, weak reduction
Thibaut Balabonski. Axiomatic sharing-via-labelling. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan, pages 85--100, 2012. [ bib | DOI | .pdf ]
A judicious use of labelled terms makes it possible to bring together the simplicity of term rewriting and the sharing power of graph rewriting: this has been known for twenty years in the particular case of orthogonal first-order systems. The present paper introduces a concise and easily usable axiomatic presentation of sharing-via-labelling techniques that applies to higher-order term rewriting as well as to non-orthogonal term rewriting. This provides a general framework for the sharing of subterms and keeps the formalism as simple as term rewriting.

Keywords: sharing, abstract term rewriting, graphs, higher order, non-orthogonality
Thibaut Balabonski and Emmanuel Haucourt. A geometric approach to the problem of unique decomposition of processes. In CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings, pages 132--146, 2010. [ bib | DOI | .pdf ]
This paper proposes a geometric solution to the problem of prime decomposability of concurrent processes first explored by R. Milner and F. Moller in [MM93]. Concurrent programs are given a geometric semantics using cubical areas, for which a unique factorization theorem is proved. An effective factorization method which is correct and complete with respect to the geometric semantics is derived from the factorization theorem. This algorithm is implemented in the static analyzer ALCOOL.

Keywords: concurrency, Milner problem, decomposition of processes, geometric semantics
Thibaut Balabonski. Optimality for dynamic patterns. In Proceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 26-28, 2010, Hagenberg, Austria, pages 231--242, 2010. [ bib | DOI | .pdf ]
Evaluation of a weak calculus featuring expressive pattern matching mechanisms is investigated by means of the construction of an efficient model of sharing. The sharing theory and its graph implementation are based on a labelling system derived from an analysis of causality relations between evaluation steps. The labelled calculus enjoys properties of confluence and finite developments, and is also used for proving correctness and optimality of a whole set of reduction strategies.

Keywords: dynamic patterns, evaluation strategies, labelled calculi, optimality, pattern matching, sharing
Thibaut Balabonski. On the implementation of dynamic patterns. In Proceedings 5th International Workshop on Higher-Order Rewriting, HOR 2010, Edinburgh, UK, July 14, 2010., pages 16--30, 2010. [ bib | DOI | .pdf ]
The evaluation mechanism of pattern matching with dynamic patterns is modelled in the Pure Pattern Calculus by one single meta-rule. This contribution presents a refinement which narrows the gap between the abstract calculus and its implementation. A calculus is designed to allow reasoning on matching algorithms. The new calculus is proved to be confluent, and to simulate the original Pure Pattern Calculus. A family of new, matching-driven, reduction strategies is proposed.

This file was generated by bibtex2html 1.98.