The OCaml Planet

[OCaML'23] Buck2 for OCaml Users & Developers Shayne Fletcher, Neil Mitchell Buck2 is an open-source large scale build system used by thousands of developers at Meta every day. Buck2 can be used to build OCaml with some useful advantages over alternatives (e.g. Dune or Bazel). In this talk we’ll discuss what those advantages are, why they arise, and how to use Buck2 for your OCaml development.

[OCaML'23] Buck2 for OCaml Users & Developers Shayne Fletcher, Neil Mitchell Buck2 is an open-source large scale build system used by thousands of developers at Meta every day. Buck2 can be used to build OCaml with some useful advantages over alternatives (e.g. Dune or Bazel). In this talk we’ll discuss what those advantages are, why they arise, and how to use Buck2 for your OCaml development.

[OCaML'23] MetaOCaml Theory and Implementation Oleg Kiselyov Quasi-quotation (or, code templates) has long been used as a convenient tool for code generation, commonly implemented as a pre-processing/translation into code-generation combinators. The original MetaOCaml was also based on such translation, done post type checking. BER MetaOCaml employs a significantly different, efficient (especially in version N114) translation integrated with type-checking, in the least intrusive way. This paper presents the integrated efficient translation for the first time.

[OCaML'23] MetaOCaml Theory and Implementation Oleg Kiselyov Quasi-quotation (or, code templates) has long been used as a convenient tool for code generation, commonly implemented as a pre-processing/translation into code-generation combinators. The original MetaOCaml was also based on such translation, done post type checking. BER MetaOCaml employs a significantly different, efficient (especially in version N114) translation integrated with type-checking, in the least intrusive way. This paper presents the integrated efficient translation for the first time.

[OCaML'23] Owi: an interpreter and a toolkit for WebAssembly written in OCaml Léo Andrès, Pierre Chambart, Eric Patrizio, Dario Pinto This presentation introduces Owi, an OCaml-based interpreter and toolkit for WebAssembly (Wasm). Owi aims to provide a fast and easily maintainable solution for Wasm code execution. Unlike competing interpreters, Owi focuses on facilitating experimentation, research, and symbolic manipulations of Wasm. We describe the different passes and intermediate representations of Owi. Additionally, we discuss the linker, the interpreter and its support for various Wasm-specific extensions. Owi’s API leverages Generalized Algebraic Data Types (GADTs) for improved error detection at link-time. We also describe the testing methods used, including a Crowbar-based fuzzer. Future work includes incorporating missing Wasm extensions, implementing advanced optimization passes, and potentially porting the WASP execution engine to perform concolic execution.

[OCaML'23] Owi: an interpreter and a toolkit for WebAssembly written in OCaml Léo Andrès, Pierre Chambart, Eric Patrizio, Dario Pinto This presentation introduces Owi, an OCaml-based interpreter and toolkit for WebAssembly (Wasm). Owi aims to provide a fast and easily maintainable solution for Wasm code execution. Unlike competing interpreters, Owi focuses on facilitating experimentation, research, and symbolic manipulations of Wasm. We describe the different passes and intermediate representations of Owi. Additionally, we discuss the linker, the interpreter and its support for various Wasm-specific extensions. Owi’s API leverages Generalized Algebraic Data Types (GADTs) for improved error detection at link-time. We also describe the testing methods used, including a Crowbar-based fuzzer. Future work includes incorporating missing Wasm extensions, implementing advanced optimization passes, and potentially porting the WASP execution engine to perform concolic execution.

[OCaML'23] Building a lock-free STM for OCaml Vesa Karvonen, Bartosz Modelski, Carine Morel, Thomas Leonard, KC Sivaramakrishnan, YSS Narasimha Naidu, Sudha Parimala The kcas library was originally developed to provide a primitive atomic lock-free multi-word compare-and-set operation. This talk introduces kcas and discusses the recent development of kcas turning it into a proper lock-free software transactional memory implementation for OCaml that provides composable transactions, scheduler friendly modular blocking, and comes with a companion library of composable lock-free data structures.

[OCaML'23] Building a lock-free STM for OCaml Vesa Karvonen, Bartosz Modelski, Carine Morel, Thomas Leonard, KC Sivaramakrishnan, YSS Narasimha Naidu, Sudha Parimala The kcas library was originally developed to provide a primitive atomic lock-free multi-word compare-and-set operation. This talk introduces kcas and discusses the recent development of kcas turning it into a proper lock-free software transactional memory implementation for OCaml that provides composable transactions, scheduler friendly modular blocking, and comes with a companion library of composable lock-free data structures.

[OCaML'23] Targeted Static Analysis for OCaml C Stubs: Eliminating gremlins from the code Edwin Török Migration to OCaml 5 requires updating a lot of C bindings due to the removal of naked pointer support. Writing OCaml user-defined primitives in C is a necessity, but is unsafe and error-prone. It does not benefit from either OCaml’s or C’s type checking, and existing C static analysers are not aware of the OCaml GC safety rules, and cannot infer them from existing macros alone. The alternative is automatically generating C stubs, which requires correctly managing value lifetimes. Having a static analyser for OCaml to C interfaces is useful outside the OCaml 5 porting effort too. After some motivating examples of real bugs in C bindings a static analyser is presented that finds these known classes of bugs. The tool works on the OCaml abstract parse and typed trees, and generates a header file and a caller model. Together with a simplified model of the OCaml runtime this is used as input to a static analysis framework, Goblint. An analysis is developed that tracks dereferences of OCaml values, and together with the existing framework reports incorrect dereferences. An example is shown how to extend the analysis to cover more safety properties. The tools and runtime models are generic and could be reused with other static analysis tools.

[OCaML'23] Targeted Static Analysis for OCaml C Stubs: Eliminating gremlins from the code Edwin Török Migration to OCaml 5 requires updating a lot of C bindings due to the removal of naked pointer support. Writing OCaml user-defined primitives in C is a necessity, but is unsafe and error-prone. It does not benefit from either OCaml’s or C’s type checking, and existing C static analysers are not aware of the OCaml GC safety rules, and cannot infer them from existing macros alone. The alternative is automatically generating C stubs, which requires correctly managing value lifetimes. Having a static analyser for OCaml to C interfaces is useful outside the OCaml 5 porting effort too. After some motivating examples of real bugs in C bindings a static analyser is presented that finds these known classes of bugs. The tool works on the OCaml abstract parse and typed trees, and generates a header file and a caller model. Together with a simplified model of the OCaml runtime this is used as input to a static analysis framework, Goblint. An analysis is developed that tracks dereferences of OCaml values, and together with the existing framework reports incorrect dereferences. An example is shown how to extend the analysis to cover more safety properties. The tools and runtime models are generic and could be reused with other static analysis tools.