 [VafeiadisBalabonskiChakrabortyMorissetZappaNardelliC11CompPOPL15]

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 SIGPLANSIGACT Symposium on
Principles of Programming Languages, POPL 2015, Mumbai, India, January 1517, 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 sourcetosource 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.
 [BalabonskiPottierProtzenkoDRFMezzoFLOPS14]

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 46, 2014. Proceedings, pages
253269, 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 sharedmemory 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 welltyped programs do not go wrong and are datarace free. Our definitions and proofs are machinechecked.
 [BalabonskiWeakOptimalityICFP13]

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
263274, 2013.
[ bib 
DOI 
.pdf ]
In this paper we investigate laziness and optimal evaluation strategies for functional programming languages. We consider the weak lambdacalculus as a basis of functional programming languages, and we adapt to this setting the concepts of optimal reductions that were defined for the full lambdacalculus. We prove that the usual implementation of callbyneed using sharing is optimal, that is, normalizing any lambdaterm with callbyneed requires exactly the same number of reduction steps as the shortest reduction sequence in the weak lambdacalculus 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
 [BalabonskiFullLazinessPOPL12]

Thibaut Balabonski.
A unified approach to fully lazy sharing.
In Proceedings of the 39th ACM SIGPLANSIGACT Symposium on
Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania,
USA, January 2228, 2012, pages 469480, 2012.
[ bib 
DOI 
.pdf ]
We give an axiomatic presentation of sharingvialabelling for weak lambdacalculi, 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 betareductions performed, although they behave differently regarding the duplication of terms. We establish a link between the optimality theories of weak lambdacalculi and firstorder rewriting systems by expressing fully lazy lambdalifting in our framework, thus emphasizing the firstorder essence of weak reduction.
Keywords: evaluation strategies, full laziness, labelling, lambdacalculus, lambdalifting, optimality, rewriting, sharing, weak reduction
 [BalabonskiSharingRTA12]

Thibaut Balabonski.
Axiomatic sharingvialabelling.
In 23rd International Conference on Rewriting Techniques and
Applications (RTA'12) , RTA 2012, May 28  June 2, 2012, Nagoya, Japan,
pages 85100, 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 firstorder systems. The present paper introduces a concise and easily usable axiomatic presentation of sharingvialabelling techniques that applies to higherorder term rewriting as well as to nonorthogonal 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, nonorthogonality
 [BalabonskiHaucourtGeometricDecompositionCONCUR10]

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 31September 3, 2010.
Proceedings, pages 132146, 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
 [BalabonskiDynamicPatternsPPDP10]

Thibaut Balabonski.
Optimality for dynamic patterns.
In Proceedings of the 12th International ACM SIGPLAN
Conference on Principles and Practice of Declarative Programming, July 2628,
2010, Hagenberg, Austria, pages 231242, 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
 [BalabonskiDynamicPatternsHOR10]

Thibaut Balabonski.
On the implementation of dynamic patterns.
In Proceedings 5th International Workshop on HigherOrder
Rewriting, HOR 2010, Edinburgh, UK, July 14, 2010., pages 1630, 2010.
[ bib 
DOI 
.pdf ]
The evaluation mechanism of pattern matching with dynamic patterns is modelled in the Pure Pattern Calculus by one single metarule. 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, matchingdriven, reduction strategies is proposed.
This file was generated by bibtex2html 1.98.