Publications

I have published in various journals and conferences on topics related to concurrency theory, system design and functional programming languages. DBLP, Research Gate and Google Scholar lists some of my publications. Or see below the full list of my journal, conference and workshop papers and technical reports.


Journals, Conferences and Workshops

2015The State of the OCaml Platform.
OCaml Workshop 2015.
2015Persistent Networking with Irmin and MirageOS.
OCaml Workskop 2015.
2015Jitsu: Just-In-Time Summoning of Unikernels.
12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15).
Abstract. Network latency is a problem for all cloud services. It can be mitigated by moving computation out of remote datacenters by rapidly instantiating local services near the user. This requires an embedded cloud platform on which to deploy multiple applications securely and quickly. We present Jitsu, a new Xen toolstack that satisfies the demands of secure multi-tenant isolation on resource-constrained embedded ARM devices. It does this by using unikernels: lightweight, compact, single address space, memory-safe virtual machines (VMs) written in a high-level language. Using fast shared memory channels, Jitsu provides a directory service that launches unikernels in response to network traffic and masks boot latency. Our evaluation shows Jitsu to be a power-efficient and responsive platform for hosting cloud services in the edge network while preserving the strong isolation guarantees of a type-1 hypervisor.
2015Mergeable Persistent Data Structures.
Les vingt-sixième Journées Francophones des Langages Applicatifs.
2014Diagnosis from Scenarios.
Journal of Discrete Event Dynamic Systems. Volume 24, Issue 4 , pp 353-415.
Abstract. Diagnosis of a system consists in providing explanations to a supervisor from a partial observation of the system and a model of possible executions. This paper proposes a partial order diagnosis algorithm that recovers sets of scenarios which correspond to a given observation. Systems are modeled using High-level Message Sequence Charts (HMSCs), and the diagnosis is given as a new HMSC, which behaviors are all explanations of the partial observation. The main difficulty is that some actions of the monitored system are unobservable but may still induce some causal ordering among observed events. We first give an offline centralized diagnosis algorithm, then we discuss a decentralized version of this algorithm. We then give an online diagnosis algorithm, and define syntactic criteria under which the memory used can be bounded. This allows us to give a complete diagnosis framework for infinite state systems, with a strong emphasis on concurrency and causal ordering in behaviors. The last contribution of the paper is an application of diagnosis techniques to a security problem called anomaly detection. Anomaly detection consists in comparing what occurs in the system with usual/expected behaviors, and raising an alarm when some unusual behavior (meaning a potential attack) occurs.
2014Metaprogramming with ML modules in the MirageOS.
ML Family Workshop.
2014The OCaml Platform v1.0.
The OCaml User and Developper Workshop.
2014Irmin: a branch-consistent distributed library database.
The OCaml User and Developper Workshop.
2013Unikernels: Library Operating Systems for the Cloud.
The 18th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2013).
Abstract. We present unikernels, a new approach to deploying cloud services via applications written in high-level source code. Unikernels are single-purpose appliances that are compile-time specialised into standalone kernels, and sealed against modification when deployed to a cloud platform. In return they offer significant reduction in image sizes, improved efficiency and security, and should reduce operational costs. Our Mirage prototype compiles OCaml code into unikernels that run on commodity clouds and offer an order of magnitude reduction in code size without significant performance penalty. The architecture combines static type-safety with a single address-space layout that can be made immutable via a hypervisor extension. Mirage contributes a suite of type-safe protocol libraries, and our results demonstrate that the hypervisor is a platform that overcomes the hardware compatibility issues that have made past library operating systems impractical to deploy in the real-world.
2013The OCaml Platform v0.1.
The OCaml User and Developper Workshop.
2013Ocamlot: OCaml Online Testing.
The OCaml User and Developper Workshop.
2013Profiling the Memory Usage of OCaml Applications without Changing their Behavior.
The OCaml User and Developper Workshop.
2012OPAM, a package manager for OCaml.
The OCaml User and Developper Workshop.
2012Study of OCaml programs' memory behavior.
The OCaml User and Developper Workshop.
2012Gestion de projet avec ocp-build.
Les vingt troisièmes Journées Francophones des Langages Applicatifs.
2011Dynamics for ML using Meta-Programming.
Electronic Notes in Theoretical Computer Science (ENTCS).
2010Mirage: ML kernels in the Cloud.
ML Family Workshop.
2010Using Functional Programming within an Industrial Product Group: Perspectives and Perceptions.
The 15th ACM SIGPLAN International Conference on Functional Programming (ICFP 2010).
Abstract. We present a case-study of using OCaml within a large product development project, focussing on both the technical and nontechnical issues that arose as a result. We draw comparisons between the OCaml team and the other teams that worked on the project, providing comparative data on hiring patterns and crossteam code contribution.
2010Turning down the LAMP: Software Specialisation for the Cloud.
The 2nd USENIX Workshop on Hot Topics in Cloud Computing.
2010Statically-typed value persistence for ML.
The 1st Workshop on Generative Technologies.
2009OXenstored: an efficient hierarchical and transactional database using functional programming with reference cell comparisons.
The 14th ACM SIGPLAN International Conference on Functional Programming (ICFP 2009).
2009Causal Message Sequence Charts.
Theoretical Computer Science, Volume 410, Number 41.
Abstract. Scenario languages based on Message Sequence Charts (MSCs) have been widely studied in the last decade. The high expressive power of MSCs renders many basic problems concerning these languages undecidable. However, several of these problems are decidable for languages that possess a behavioral property called “existentially bounded”. Unfortunately, collections of scenarios outside this class are frequently exhibited by systems such as sliding window protocols. We propose here an extension of MSCs called causal Message Sequence Charts and a natural mechanism for defining languages of causal MSCs called causal HMSCs (CaHMSCs). These languages preserve decidable properties without requiring existential bounds. Further, they can model collections of scenarios generated by sliding window protocols. We establish here the basic theory of CaHMSCs as well as the expressive power and complexity of decision procedures for various subclasses of CaHMSCs. We also illustrate the modeling power of our formalism with the help of a realistic example based on the TCP sliding window feature.
2008Logic-based Diagnosis for Distributed Systems.
'Perspectives in Concurrency -- Feststichrift for P.S. Thiagarajan'. World Scientific.
2008Small Logs for Transactional Services: Distinction is much more accurate than (Positive) Discrimination.
The 11th IEEE High Assurance Systems Engineering Symposium.
2007Causal Message Sequence Charts.
The 18th International Conference on Concurrency Theory (CONCUR 2007).
2007Reconstructing Causal Ordering with boxed pomsets.
The 27th IFIP WG 6.1 International Conference on Formal Methods for Networked and Distributed Systems.
2007Abstraire à la Volée les Evénements d'un Système Réparti
La 7 ème Conférence Internationale sur les NOuvelles TEchnologies de la REpartition.
2006Diagnosis from Scenarios.
The 8th International Workshop on Discrete Event Systems.

Technical Reports

2008Projection of Rational Pomset Expression.
Draft.
2008Langages de Scénarios: Utiliser des Ordres Partiels pour Modéliser, Vérifier et Superviser des Systèmes Parallèles et Répartis.
Ph.D. Thesis, University of Rennes 1.
Abstract. Our work is dedicated to the modeling and the analysis of concurrent and distributed systems. More precisely, we seek to model, verify and supervise systems composed by autonomous entities which interact locally through shared memory and globally through asynchronous message passing. In this context, we argue that, instead of modeling each entity independently and then analyzing what happens when all of them interact, it is better to have a complete theory to globally describe a concurrent system, in which verification and supervision analysis are decidable. This theory is based on partially ordered multisets (ie. “pomsets”) which is a “true-concurrency” model. To this end, we defined the causal hmsc model, based on pomsets and which extends the standardized hmsc formalism with constructs from Mazurkiewicz trace theory. We first show that a syntactic restriction of causal hmsc is equivalent to bounded mixed automata, a formalism which extends Zielonka asynchronous automata and communicating finite state machines. We also show that classical model-checking techniques can be extended to pomsetsbased formalisms without losing efficacy. This is an important result, as pomsets-based formalisms, such as causal hmsc, are more concise than sequential system formalisms. Finally, we propose efficient methods to analyse large recorded files from distributed executions and we propose supervision techniques such as diagnosis and event correlation, using pomsets-based models of distributed and concurrent systems.
2007Causal Message Sequence Charts.
Research Report RR-6301.
2005Online Abstraction of Distributed Executions.
Research Report RR-5736.