Wiki Agenda Contact Version française

Publications : Arthur Charguéraud

[18] Arthur Charguéraud and François Pottier. Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. Journal of Automated Reasoning, September 2017. [ bib | .pdf ]
Union-Find is a famous example of a simple data structure whose amortized asymptotic time complexity analysis is nontrivial. We present a Coq formalization of this analysis, following Alstrup et al.'s recent proof (2014). Moreover, we implement Union-Find as an OCaml library and formally endow it with a modular specification that offers a full functional correctness guarantee as well as an amortized complexity bound. In order to reason in Coq about imperative OCaml code, we use the CFML tool, which implements Separation Logic for a subset of OCaml, and which we extend with time credits. Although it was known in principle that amortized analysis can be explained in terms of time credits and that time credits can be viewed as resources in Separation Logic, we believe our work is the first practical demonstration of this approach. Finally, in order to explain the meta-theoretical foundations of our approach, we define a Separation Logic with time credits for an untyped call-by-value lambda-calculus, and formally verify its soundness.

[17] Arthur Charguéraud, Jean-Christophe Filliâtre, Mário Pereira, and François Pottier. VOCAL -- A Verified OCaml Library. ML Family Workshop, September 2017. [ bib | full text on HAL ]
[16] Umut A Acar, Arthur Charguéraud, and Mike Rainey. Oracle-guided scheduling for controlling granularity in implicitly parallel languages. Journal of Functional Programming, 26, November 2016. [ bib | DOI | full text on HAL ]
[15] Umut A Acar, Arthur Charguéraud, Mike Rainey, and Filip Sieczkowski. Dag-calculus: a calculus for parallel computation. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 18--32, Nara, Japan, September 2016. [ bib | DOI | full text on HAL ]
[14] Arthur Charguéraud. Higher-Order Representation Predicates in Separation Logic. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, Florida, United States, January 2016. [ bib | full text on HAL ]
[13] Umut A. Acar, Arthur Charguéraud, and Mike Rainey. A Work-Efficient Algorithm for Parallel Unordered Depth-First Search. In Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, Austin, Texas, United States, November 2015. [ bib | DOI | full text on HAL | http ]
[12] Arthur Charguéraud and François Pottier. Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. In 6th International Conference on Interactive Theorem Proving (ITP), Nanjing, China, August 2015. [ bib | DOI | full text on HAL | http ]
[11] Umut A. Acar, Arthur Charguéraud, and Mike Rainey. Fast parallel graph-search with splittable and catenable frontiers. Technical report, Inria, January 2015. [ bib | full text on HAL ]
[10] Umut A. Acar, Arthur Charguéraud, and Mike Rainey. Theory and practice of chunked sequences. In AndreasS. Schulz and Dorothea Wagner, editors, European Symposium on Algorithms, volume Lecture Notes in Computer Science, pages 25--36, Wroclaw, Poland, September 2014. Springer. [ bib | DOI | full text on HAL ]
Keywords: Data structure ; Sequence ; Chunk ; Amortization
[9] M. Bodin, A. Charguéraud, D. Filaretti, P. Gardner, S. Maffeis, D. Naudziuniene, A. Schmitt, and G. Smith. A trusted mechanised JavaScript specification. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, USA, January 2014. ACM Press. [ bib | full text on HAL ]
[8] Umut A. Acar, Arthur Charguéraud, Stefan Muller, and Mike Rainey. Atomic read-modify-write operations are unnecessary for shared-memory work stealing. Research report, HAL, September 2013. [ bib | full text on HAL ]
We present a work-stealing algorithm for total-store memory architectures, such as Intel's X86, that does not rely on atomic read-modify-write instructions such as compare-and-swap. In our algorithm, processors communicate solely by reading from and writing (non-atomically) into weakly consistent memory. We also show that join resolution, an important problem in scheduling parallel programs, can also be solved without using atomic read-modify-write instructions. At a high level, our work-stealing algorithm closely resembles traditional work-stealing algorithms, but certain details are more complex. Instead of relying on atomic read-modify-write operations, our algorithm uses a steal protocol that enables processors to perform load balancing by using only two memory cells per processor. The steal protocol permits data races but guarantees correctness by using a time-stamping technique. Proving the correctness of our algorithms is made challenging by weakly consistent shared-memory that permits processors to observe sequentially inconsistent views. We therefore carefully specify our algorithms and prove them correct by considering a costed refinement of the X86-TSO model, a precise characterization of total-store-order architectures. We show that our algorithms are practical by implementing them as part of a C++ library and performing an experimental evaluation. Our results show that our work-stealing algorithm is competitive with the state-of-the-art implementations even on current architectures where atomic read-modify-write instructions are cheap. Our join resolution algorithm incurs a relatively small overhead compared to an efficient algorithm that uses atomic read-modify-write instructions.

[7] Arthur Charguéraud. Pretty-big-step semantics. In Matthias Felleisen and Philippa Gardner, editors, Proceedings of the 22nd European Symposium on Programming, volume 7792 of Lecture Notes in Computer Science, pages 41--60. Springer, March 2013. [ bib | full text on HAL ]
[6] Umut A. Acar, Arthur Charguéraud, and Mike Rainey. Scheduling parallel programs by work stealing with private deques. In Proceedings of the 18th ACM SIGPLAN symposium on Principles and practice of parallel programming, PPoPP '13, pages 219--228. ACM Press, February 2013. [ bib | DOI | full text on HAL ]
[5] Umut A. Acar, Arthur Charguéraud, and Mike Rainey. Efficient primitives for creating and scheduling parallel computations. In Declarative Aspects and Applications of Multicore Programming (DAMP), January 2012. [ bib ]
[4] Umut A. Acar, Arthur Charguéraud, and Mike Rainey. Oracle scheduling: Controlling granularity in implicitly parallel languages. In Cristina Videira Lopes and Kathleen Fisher, editors, Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, (OOPSLA), pages 499--518. ACM, October 2011. [ bib | http ]
[3] Arthur Charguéraud. Characteristic formulae for the verification of imperative programs. In Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy, editors, Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming (ICFP), pages 418--430, Tokyo, Japan, September 2011. ACM. [ bib ]
[2] Arthur Charguéraud. Characteristic Formulae for Mechanized Program Verification. PhD thesis, Université Paris 7, 2010. [ bib ]
[1] Arthur Charguéraud and François Pottier. Functional translation of a calculus of capabilities. In ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 213--224, September 2008. [ bib | DOI | .pdf ]
Reasoning about imperative programs requires the ability to track aliasing and ownership properties. We present a type system that provides this ability, by using regions, capabilities, and singleton types. It is designed for a high-level calculus with higher-order functions, algebraic data structures, and references (mutable memory cells). The type system has polymorphism, yet does not require a value restriction, because capabilities act as explicit store typings.

We exhibit a type-directed, type-preserving, and meaning-preserving translation of this imperative calculus into a pure calculus. Like the monadic translation, this is a store-passing translation. Here, however, the store is partitioned into multiple fragments, which are threaded through a computation only if they are relevant to it. Furthermore, the decomposition of the store into fragments can evolve dynamically to reflect ownership transfers.

The translation offers deep insight about the inner workings and soundness of the type system. If coupled with a semantic model of its target calculus, it leads to a semantic model of its imperative source calculus. Furthermore, it provides a foundation for our long-term objective of designing a system for specifying and certifying imperative programs with dynamic memory allocation.

This page was generated by bibtex2html.