Publications : Arthur Charguéraud
Back[20]  Arthur Charguéraud, JeanChristophe Filliâtre, Cláudio Belo Lourenço, and Mário Pereira. GOSPEL  providing OCaml with a formal specification language. In Annabelle McIver and Maurice ter Beek, editors, FM 2019 23rd International Symposium on Formal Methods, Porto, Portugal, October 2019. [ bib  full text on HAL ] 
[19] 
Arthur Charguéraud and François Pottier.
Verifying the correctness and amortized complexity of a unionfind
implementation in separation logic with time credits.
Journal of Automated Reasoning, 62(3):331365, March 2019.
[ bib 
.pdf ]
UnionFind 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 UnionFind 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 metatheoretical foundations of our approach, we define a Separation Logic with time credits for an untyped callbyvalue lambdacalculus, and formally verify its soundness.

[18]  Armaël Guéneau, Arthur Charguéraud, and François Pottier. A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification. In ESOP 2018  27th European Symposium on Programming, volume 10801 of Lecture Notes in Computer Science. Springer, 2018. [ bib  DOI ] 
[17]  Arthur Charguéraud, JeanChristophe 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. Oracleguided 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. Dagcalculus: a calculus for parallel computation. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 1832, Nara, Japan, September 2016. [ bib  DOI  full text on HAL ] 
[14]  Arthur Charguéraud. HigherOrder 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 WorkEfficient Algorithm for Parallel Unordered DepthFirst 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. MachineChecked Verification of the Correctness and Amortized Complexity of an Efficient UnionFind 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 graphsearch 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 8737 of Lecture Notes in Computer
Science, pages 2536, 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 SIGPLANSIGACT 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 readmodifywrite operations are unnecessary for sharedmemory
work stealing.
Research report, HAL, September 2013.
[ bib 
full text on HAL ]
We present a workstealing algorithm for totalstore memory architectures, such as Intel's X86, that does not rely on atomic readmodifywrite instructions such as compareandswap. In our algorithm, processors communicate solely by reading from and writing (nonatomically) into weakly consistent memory. We also show that join resolution, an important problem in scheduling parallel programs, can also be solved without using atomic readmodifywrite instructions. At a high level, our workstealing algorithm closely resembles traditional workstealing algorithms, but certain details are more complex. Instead of relying on atomic readmodifywrite 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 timestamping technique. Proving the correctness of our algorithms is made challenging by weakly consistent sharedmemory 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 X86TSO model, a precise characterization of totalstoreorder 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 workstealing algorithm is competitive with the stateoftheart implementations even on current architectures where atomic readmodifywrite instructions are cheap. Our join resolution algorithm incurs a relatively small overhead compared to an efficient algorithm that uses atomic readmodifywrite instructions.

[7]  Arthur Charguéraud. Prettybigstep 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 4160. 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 219228. 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 ObjectOriented Programming, Systems, Languages, and Applications, (OOPSLA), pages 499518. 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 418430, Tokyo, Japan, September 2011. ACM. [ bib ] 
[2]  Arthur Charguéraud. Characteristic Formulae for Mechanized Program Verification. PhD thesis, Université Paris 7, 2010. http://www.chargueraud.org/arthur/research/2010/thesis/. [ 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 213224, 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 highlevel calculus with higherorder 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.

Back
This page was generated by bibtex2html.