From cf98a1b5e927d002d192c950c08d6f60e30e3044 Mon Sep 17 00:00:00 2001 From: christinerose Date: Wed, 13 Nov 2024 05:50:23 +0000 Subject: [PATCH] [scrape.yml] New OCaml Planet blog posts and videos from watch.ocaml.org --- .../cwn/ocaml-weekly-news-01-oct-2024.md | 12 + .../cwn/ocaml-weekly-news-05-nov-2024.md | 12 + .../cwn/ocaml-weekly-news-08-oct-2024.md | 12 + .../cwn/ocaml-weekly-news-10-sep-2024.md | 12 + .../cwn/ocaml-weekly-news-12-nov-2024.md | 12 + .../cwn/ocaml-weekly-news-15-oct-2024.md | 12 + .../cwn/ocaml-weekly-news-17-sep-2024.md | 12 + .../cwn/ocaml-weekly-news-22-oct-2024.md | 12 + .../cwn/ocaml-weekly-news-24-sep-2024.md | 12 + .../cwn/ocaml-weekly-news-29-oct-2024.md | 12 + data/planet/dinosaure/happy-eyeballs.md | 12 + .../emillon/introducing-tree-sitter-dune.md | 90 ++ data/planet/emilpriver/why-i-like-ocaml.md | 374 +++++++ .../beta-release-of-frama-c-300beta-zinc.md | 12 + ...rama-clang-v0016-for-frama-c-290-copper.md | 12 + .../metacsl-v07-for-frama-c-290-copper.md | 12 + ...-verification-with-frama-c-is-available.md | 12 + ...nted-at-frama-c-days-2024-are-available.md | 12 + .../developer-education-at-jane-street.md | 20 + data/planet/janestreet/icfp-2024.md | 22 + ...lizing-piecewise-linear-neural-networks.md | 15 + ...t-the-interns-have-wrought-2024-edition.md | 16 + data/planet/ocamlpro/alt-ergo-26-is-out.md | 246 +++++ .../flambda2-ep-3-speculative-inlining-.md | 472 +++++++++ data/planet/ocamlpro/opam-220-release.md | 246 +++++ ...ranais-de-gnalogie-depuis-prs-de-30-ans.md | 54 + ...b-to-the-trading-floor-with-erin-murphy.md | 13 + ...zles-in-production-with-liora-friedberg.md | 13 + ...elerating-ml-models-with-sylvain-gugger.md | 13 + .../talex5/ocaml-5-performance-part-2.md | 959 ++++++++++++++++++ .../talex5/ocaml-5-performance-problems.md | 524 ++++++++++ ...mand---part-3-vscode-platform-extension.md | 197 ++++ ...-optimising-multicore-ocaml-for-windows.md | 53 + ...l-compiler-with-dune-package-management.md | 21 + ...ement-revolutionising-ocaml-development.md | 32 + .../easy-debugging-for-ocaml-with-lldb.md | 23 + ...pective-an-interview-with-simon-grondin.md | 52 + ...eature-parity-series-compaction-is-back.md | 59 ++ ...nnouncing-the-gospel-and-ortac-projects.md | 54 + ...caml-better-data-races-caught-and-fixed.md | 46 + ...ntial-build-system-for-ocaml-developers.md | 39 + ...oviding-observability-tools-for-ocaml-5.md | 35 + ...preview-a-new-era-for-ocaml-development.md | 34 + ...your-handy-guide-to-ocaml-documentation.md | 46 + .../looking-back-on-our-experience-at-icfp.md | 49 + ...pto-safer-introducing-the-argos-project.md | 36 + ...-support-our-open-source-work-on-github.md | 56 + ...f-unchecked-complexity-in-cybersecurity.md | 44 + .../ocaml-compiler-manual-html-generation.md | 99 ++ ...w-navigation-feature-for-ocaml-52-users.md | 153 +++ ...s-projects-from-the-ocaml-compiler-team.md | 36 + ...f-the-year-what-are-we-bringing-to-icfp.md | 44 + ...mentals-functional-programming-and-more.md | 55 + ...aml23-buck2-for-ocaml-users--developers.md | 17 + ...ml23-building-a-lock-free-stm-for-ocaml.md | 17 + ...icient-ocaml-compilation-with-flambda-2.md | 17 + ...23-eio-10--effects-based-io-for-ocaml-5.md | 17 + ...g-ocaml-features-for-effective-teaching.md | 19 + ...l23-metaocaml-theory-and-implementation.md | 17 + ...ure-in-ocaml-our-experience-with-catala.md | 20 + ...s-an-iris-based-program-logic-for-ocaml.md | 17 + ...oolkit-for-webassembly-written-in-ocaml.md | 17 + ...3-parallel-sequences-in-multicore-ocaml.md | 17 + ...caml23-state-of-the-ocaml-platform-2023.md | 18 + ...tubs-eliminating-gremlins-from-the-code.md | 20 + .../watch-ocaml/outreachy-may-2024-demo.md | 16 + data/watch.yml | 170 ++++ 67 files changed, 4931 insertions(+) create mode 100644 data/planet/cwn/ocaml-weekly-news-01-oct-2024.md create mode 100644 data/planet/cwn/ocaml-weekly-news-05-nov-2024.md create mode 100644 data/planet/cwn/ocaml-weekly-news-08-oct-2024.md create mode 100644 data/planet/cwn/ocaml-weekly-news-10-sep-2024.md create mode 100644 data/planet/cwn/ocaml-weekly-news-12-nov-2024.md create mode 100644 data/planet/cwn/ocaml-weekly-news-15-oct-2024.md create mode 100644 data/planet/cwn/ocaml-weekly-news-17-sep-2024.md create mode 100644 data/planet/cwn/ocaml-weekly-news-22-oct-2024.md create mode 100644 data/planet/cwn/ocaml-weekly-news-24-sep-2024.md create mode 100644 data/planet/cwn/ocaml-weekly-news-29-oct-2024.md create mode 100644 data/planet/dinosaure/happy-eyeballs.md create mode 100644 data/planet/emillon/introducing-tree-sitter-dune.md create mode 100644 data/planet/emilpriver/why-i-like-ocaml.md create mode 100644 data/planet/frama-c/beta-release-of-frama-c-300beta-zinc.md create mode 100644 data/planet/frama-c/frama-clang-v0016-for-frama-c-290-copper.md create mode 100644 data/planet/frama-c/metacsl-v07-for-frama-c-290-copper.md create mode 100644 data/planet/frama-c/the-guide-to-software-verification-with-frama-c-is-available.md create mode 100644 data/planet/frama-c/the-slides-presented-at-frama-c-days-2024-are-available.md create mode 100644 data/planet/janestreet/developer-education-at-jane-street.md create mode 100644 data/planet/janestreet/icfp-2024.md create mode 100644 data/planet/janestreet/visualizing-piecewise-linear-neural-networks.md create mode 100644 data/planet/janestreet/what-the-interns-have-wrought-2024-edition.md create mode 100644 data/planet/ocamlpro/alt-ergo-26-is-out.md create mode 100644 data/planet/ocamlpro/flambda2-ep-3-speculative-inlining-.md create mode 100644 data/planet/ocamlpro/opam-220-release.md create mode 100644 data/planet/ocamlpro/optimisation-de-geneweb-1er-logiciel-franais-de-gnalogie-depuis-prs-de-30-ans.md create mode 100644 data/planet/signalsandthreads/from-the-lab-to-the-trading-floor-with-erin-murphy.md create mode 100644 data/planet/signalsandthreads/solving-puzzles-in-production-with-liora-friedberg.md create mode 100644 data/planet/signalsandthreads/the-uncertain-art-of-accelerating-ml-models-with-sylvain-gugger.md create mode 100644 data/planet/talex5/ocaml-5-performance-part-2.md create mode 100644 data/planet/talex5/ocaml-5-performance-problems.md create mode 100644 data/planet/tarides/creating-the-syntaxdocumentation-command---part-3-vscode-platform-extension.md create mode 100644 data/planet/tarides/deep-dive-optimising-multicore-ocaml-for-windows.md create mode 100644 data/planet/tarides/dune-developer-preview-installing-the-ocaml-compiler-with-dune-package-management.md create mode 100644 data/planet/tarides/dune-package-management-revolutionising-ocaml-development.md create mode 100644 data/planet/tarides/easy-debugging-for-ocaml-with-lldb.md create mode 100644 data/planet/tarides/eio-from-a-users-perspective-an-interview-with-simon-grondin.md create mode 100644 data/planet/tarides/feature-parity-series-compaction-is-back.md create mode 100644 data/planet/tarides/getting-specific-announcing-the-gospel-and-ortac-projects.md create mode 100644 data/planet/tarides/how-tsan-makes-ocaml-better-data-races-caught-and-fixed.md create mode 100644 data/planet/tarides/introducing-dune-the-essential-build-system-for-ocaml-developers.md create mode 100644 data/planet/tarides/introducing-olly-providing-observability-tools-for-ocaml-5.md create mode 100644 data/planet/tarides/introducing-the-dune-developer-preview-a-new-era-for-ocaml-development.md create mode 100644 data/planet/tarides/introducing-the-odoc-cheatsheet-your-handy-guide-to-ocaml-documentation.md create mode 100644 data/planet/tarides/looking-back-on-our-experience-at-icfp.md create mode 100644 data/planet/tarides/making-crypto-safer-introducing-the-argos-project.md create mode 100644 data/planet/tarides/making-ocaml-mainstream-support-our-open-source-work-on-github.md create mode 100644 data/planet/tarides/monoculture-of-insecurity-how-crowdstrikes-outage-exposes-the-risks-of-unchecked-complexity-in-cybersecurity.md create mode 100644 data/planet/tarides/ocaml-compiler-manual-html-generation.md create mode 100644 data/planet/tarides/project-wide-occurrences-a-new-navigation-feature-for-ocaml-52-users.md create mode 100644 data/planet/tarides/summer-of-internships-projects-from-the-ocaml-compiler-team.md create mode 100644 data/planet/tarides/the-biggest-functional-programming-conference-of-the-year-what-are-we-bringing-to-icfp.md create mode 100644 data/planet/tarides/unlock-your-teams-potential-with-expert-training-in-ocaml-cybersecurity-fundamentals-functional-programming-and-more.md create mode 100644 data/planet/watch-ocaml/ocaml23-buck2-for-ocaml-users--developers.md create mode 100644 data/planet/watch-ocaml/ocaml23-building-a-lock-free-stm-for-ocaml.md create mode 100644 data/planet/watch-ocaml/ocaml23-efficient-ocaml-compilation-with-flambda-2.md create mode 100644 data/planet/watch-ocaml/ocaml23-eio-10--effects-based-io-for-ocaml-5.md create mode 100644 data/planet/watch-ocaml/ocaml23-less-power-for-more-learning-restricting-ocaml-features-for-effective-teaching.md create mode 100644 data/planet/watch-ocaml/ocaml23-metaocaml-theory-and-implementation.md create mode 100644 data/planet/watch-ocaml/ocaml23-modern-dsl-compiler-architecture-in-ocaml-our-experience-with-catala.md create mode 100644 data/planet/watch-ocaml/ocaml23-osiris-an-iris-based-program-logic-for-ocaml.md create mode 100644 data/planet/watch-ocaml/ocaml23-owi-an-interpreter-and-a-toolkit-for-webassembly-written-in-ocaml.md create mode 100644 data/planet/watch-ocaml/ocaml23-parallel-sequences-in-multicore-ocaml.md create mode 100644 data/planet/watch-ocaml/ocaml23-state-of-the-ocaml-platform-2023.md create mode 100644 data/planet/watch-ocaml/ocaml23-targeted-static-analysis-for-ocaml-c-stubs-eliminating-gremlins-from-the-code.md create mode 100644 data/planet/watch-ocaml/outreachy-may-2024-demo.md diff --git a/data/planet/cwn/ocaml-weekly-news-01-oct-2024.md b/data/planet/cwn/ocaml-weekly-news-01-oct-2024.md new file mode 100644 index 0000000000..3b20ab1144 --- /dev/null +++ b/data/planet/cwn/ocaml-weekly-news-01-oct-2024.md @@ -0,0 +1,12 @@ +--- +title: OCaml Weekly News, 01 Oct 2024 +description: +url: https://alan.petitepomme.net/cwn/2024.10.01.html +date: 2024-10-01T12:00:00-00:00 +preview_image: +authors: +- Caml Weekly News +source: +--- + +
  1. Dune Developer Preview Updates
  2. Uuidm 0.9.9
  3. first release of ppx_deriving_jsonschema
  4. Bogue, the OCaml GUI
  5. New release of Merlin
  6. Releases of mirage-crypto 1.0.0, tls 1.0.0, x509 1.0.0, asn1-combinators 0.3.0, let's encrypt 1.0.0, awa 0.4.0, kdf 1.0.0, paf 0.7.0, git 3.17.0
  7. ICFP 2023 OCaml Presentations on YouTube
  8. Dune dev meeting
  9. Other OCaml News
diff --git a/data/planet/cwn/ocaml-weekly-news-05-nov-2024.md b/data/planet/cwn/ocaml-weekly-news-05-nov-2024.md new file mode 100644 index 0000000000..d54174fcad --- /dev/null +++ b/data/planet/cwn/ocaml-weekly-news-05-nov-2024.md @@ -0,0 +1,12 @@ +--- +title: OCaml Weekly News, 05 Nov 2024 +description: +url: https://alan.petitepomme.net/cwn/2024.11.05.html +date: 2024-11-05T12:00:00-00:00 +preview_image: +authors: +- Caml Weekly News +source: +--- + +
  1. GPTar 1.0.0
  2. opam 2.3.0~rc1
  3. Call for Contributions: BOB 2025 (Berlin, March 14 - Deadline Nov 15)
  4. First beta release for OCaml 5.3.0
  5. dune 3.16
  6. Other OCaml News
diff --git a/data/planet/cwn/ocaml-weekly-news-08-oct-2024.md b/data/planet/cwn/ocaml-weekly-news-08-oct-2024.md new file mode 100644 index 0000000000..c55541df5c --- /dev/null +++ b/data/planet/cwn/ocaml-weekly-news-08-oct-2024.md @@ -0,0 +1,12 @@ +--- +title: OCaml Weekly News, 08 Oct 2024 +description: +url: https://alan.petitepomme.net/cwn/2024.10.08.html +date: 2024-10-08T12:00:00-00:00 +preview_image: +authors: +- Caml Weekly News +source: +--- + +
  1. Releases of fpath-sexplib0, fpath-base, loc, file-rewriter, sexps-rewriter and provider
  2. Build a project without Stdlib
  3. obatcher: Framework for building efficient concurrent services
  4. DBLP query program and library
  5. cudajit: Bindings to the ~cuda~ and ~nvrtc~ libraries
  6. YOCaml, a framework for static site generator
  7. oepub 0.1.0 : A library to parse epub files
  8. ppx_deriving_router — type safe routing for Dream and Melange
  9. Mica, a PPX that automates differential testing for OCaml modules
  10. Simplified Android cross-compiler with DkML
  11. Other OCaml News
diff --git a/data/planet/cwn/ocaml-weekly-news-10-sep-2024.md b/data/planet/cwn/ocaml-weekly-news-10-sep-2024.md new file mode 100644 index 0000000000..4abcaa8a7b --- /dev/null +++ b/data/planet/cwn/ocaml-weekly-news-10-sep-2024.md @@ -0,0 +1,12 @@ +--- +title: OCaml Weekly News, 10 Sep 2024 +description: +url: https://alan.petitepomme.net/cwn/2024.09.10.html +date: 2024-09-10T12:00:00-00:00 +preview_image: +authors: +- Caml Weekly News +source: +--- + +
  1. Oxidizing OCaml — an update
  2. Toy Autograd Engine in OCaml with Apple Accelerate Backend
  3. New release of cppo, with multi-line macros and higher-order macros
  4. OCamlPro's contributions to the 2024 ICFP in Milan
  5. Flambda2 Ep. 3: Speculative Inlining, by OCamlPro
  6. Frustrating Interactions with the OCaml Ecosystem while developing a Synthesizer Library
  7. Cmdlang - Yet Another CLI Library (well, not really)
  8. zarr v0.1.0
  9. Brr 0.0.7
  10. Ocsigen Server 6.0.0
  11. dream-html and pure-html
  12. Advanced Code Navigation coming to OCaml-LSP
  13. Other OCaml News
diff --git a/data/planet/cwn/ocaml-weekly-news-12-nov-2024.md b/data/planet/cwn/ocaml-weekly-news-12-nov-2024.md new file mode 100644 index 0000000000..492d1f4b01 --- /dev/null +++ b/data/planet/cwn/ocaml-weekly-news-12-nov-2024.md @@ -0,0 +1,12 @@ +--- +title: OCaml Weekly News, 12 Nov 2024 +description: +url: https://alan.petitepomme.net/cwn/2024.11.12.html +date: 2024-11-12T12:00:00-00:00 +preview_image: +authors: +- Caml Weekly News +source: +--- + +
  1. Picos — Interoperable effects based concurrency
  2. findlib-1.9.7
  3. First release candidate for OCaml 5.2.1
  4. mirage-swapfs
  5. Dune dev meeting
  6. Other OCaml News
diff --git a/data/planet/cwn/ocaml-weekly-news-15-oct-2024.md b/data/planet/cwn/ocaml-weekly-news-15-oct-2024.md new file mode 100644 index 0000000000..526116c43f --- /dev/null +++ b/data/planet/cwn/ocaml-weekly-news-15-oct-2024.md @@ -0,0 +1,12 @@ +--- +title: OCaml Weekly News, 15 Oct 2024 +description: +url: https://alan.petitepomme.net/cwn/2024.10.15.html +date: 2024-10-15T12:00:00-00:00 +preview_image: +authors: +- Caml Weekly News +source: +--- + +
  1. grep_cmt: structural search of OCaml code
  2. Mutaml 0.1
  3. ocaml-activitypub
  4. Ortac/QCheck-STM 0.4.0 Dynamic formal verification beyond one system under test
  5. Openbsd 1.0
  6. Compsort - reorder files in archives for improved compression
  7. Dune dev meeting
  8. Other OCaml News
diff --git a/data/planet/cwn/ocaml-weekly-news-17-sep-2024.md b/data/planet/cwn/ocaml-weekly-news-17-sep-2024.md new file mode 100644 index 0000000000..2046954678 --- /dev/null +++ b/data/planet/cwn/ocaml-weekly-news-17-sep-2024.md @@ -0,0 +1,12 @@ +--- +title: OCaml Weekly News, 17 Sep 2024 +description: +url: https://alan.petitepomme.net/cwn/2024.09.17.html +date: 2024-09-17T12:00:00-00:00 +preview_image: +authors: +- Caml Weekly News +source: +--- + +
  1. Ptime 1.2.0 – Mtime 2.1.0 – Qrc 0.2.0
  2. Unicode 16.0.0 update for Uucd, Uucp, Uunf and Uuseg
  3. Outreachy Demo Presentation
  4. Live Stream to follow OCaml Workshop, ML Workshop, and other talks at ICFP
  5. DkML 2.1.2 and opam 2.2.0
  6. store v0.1.0
  7. Tsdl 1.1.0
  8. OCaml-css 0.2.0
  9. OCaml-stk 0.2.0 and Chamo 4.1.0
  10. DkCoder 2.1.3
  11. Other OCaml News
diff --git a/data/planet/cwn/ocaml-weekly-news-22-oct-2024.md b/data/planet/cwn/ocaml-weekly-news-22-oct-2024.md new file mode 100644 index 0000000000..f060571035 --- /dev/null +++ b/data/planet/cwn/ocaml-weekly-news-22-oct-2024.md @@ -0,0 +1,12 @@ +--- +title: OCaml Weekly News, 22 Oct 2024 +description: +url: https://alan.petitepomme.net/cwn/2024.10.22.html +date: 2024-10-22T12:00:00-00:00 +preview_image: +authors: +- Caml Weekly News +source: +--- + +
  1. opam 2.3.0~beta1
  2. Dune dev meeting
  3. Wildcard expansion on Windows
  4. OCamlformat and GitHub actions
  5. New vs. Old OCaml Academic Users Page Survey
  6. New vs. Old OCaml Industrial Users Page
  7. Eliom 11 and Ocsigen Start 7
  8. Other OCaml News
diff --git a/data/planet/cwn/ocaml-weekly-news-24-sep-2024.md b/data/planet/cwn/ocaml-weekly-news-24-sep-2024.md new file mode 100644 index 0000000000..464ab14464 --- /dev/null +++ b/data/planet/cwn/ocaml-weekly-news-24-sep-2024.md @@ -0,0 +1,12 @@ +--- +title: OCaml Weekly News, 24 Sep 2024 +description: +url: https://alan.petitepomme.net/cwn/2024.09.24.html +date: 2024-09-24T12:00:00-00:00 +preview_image: +authors: +- Caml Weekly News +source: +--- + +
  1. ocaml-trace 0.8
  2. qcheck-lin and qcheck-stm 0.2
  3. 3rd editor tooling dev-meeting: 26th of September 🧙
  4. First release of hachis
  5. OCaml Platform Newsletter: June-August 2024
  6. First alpha release of OCaml 5.3.0
  7. Ascend - Dungeon RPG for your terminal
  8. first release of ppx_deriving_jsonschema
  9. opam 2.3.0~alpha1
  10. Other OCaml News
diff --git a/data/planet/cwn/ocaml-weekly-news-29-oct-2024.md b/data/planet/cwn/ocaml-weekly-news-29-oct-2024.md new file mode 100644 index 0000000000..b746bf046e --- /dev/null +++ b/data/planet/cwn/ocaml-weekly-news-29-oct-2024.md @@ -0,0 +1,12 @@ +--- +title: OCaml Weekly News, 29 Oct 2024 +description: +url: https://alan.petitepomme.net/cwn/2024.10.29.html +date: 2024-10-29T12:00:00-00:00 +preview_image: +authors: +- Caml Weekly News +source: +--- + +
  1. HOL Light released to OPAM
  2. Could we add a tiny OCaml interpreter to Numworks graphical calculators?
  3. opam 2.3.0~beta2
  4. Editors dev-meeting #4, Thu. 31th: Search by type à la Sherlodoc 🕵️
  5. Dune dev meeting
  6. Shell Completions in Dune Developer Preview
  7. Other OCaml News
diff --git a/data/planet/dinosaure/happy-eyeballs.md b/data/planet/dinosaure/happy-eyeballs.md new file mode 100644 index 0000000000..caf1af21d3 --- /dev/null +++ b/data/planet/dinosaure/happy-eyeballs.md @@ -0,0 +1,12 @@ +--- +title: Happy eyeballs?! +description: +url: https://blog.osau.re/articles/happy_eyeballs.html +date: 2024-09-27T00:00:00-00:00 +preview_image: +authors: +- Romain Calascibetta +source: +--- + +When connect() hides a lot of details. diff --git a/data/planet/emillon/introducing-tree-sitter-dune.md b/data/planet/emillon/introducing-tree-sitter-dune.md new file mode 100644 index 0000000000..76a0283069 --- /dev/null +++ b/data/planet/emillon/introducing-tree-sitter-dune.md @@ -0,0 +1,90 @@ +--- +title: Introducing tree-sitter-dune +description: +url: http://blog.emillon.org/posts/2024-07-26-introducing-tree-sitter-dune.html +date: 2024-07-26T00:00:00-00:00 +preview_image: +authors: +- Etienne Millon +source: +--- + +

I made a tree-sitter plugin for +dune files. It is available on +GitHub.

+

Tree-sitter is a parsing system that can be used in text editors. +Dune is a build system for OCaml projects. +Its configuration language lives in dune files which use a s-expression +syntax.

+

This makes highlighting challenging: the lexing part of the language is very +simple (atoms, strings, parentheses), but it is not enough to make a good +highlighter.

+

In the following example, with-stdout-to and echo are “actions” that we +could highlight in a special way, but these names can also appear in places +where they are not interpreted as actions, and doing so would be confusing (for +example, we could write to a file named echo instead of foo.txt.

+
(rule
+ (action
+  (with-stdout-to
+   foo.txt
+   (echo "testing"))))
+

Tree-sitter solves this, because it creates an actual parser that goes beyond +lexing.

+

In this example, I created grammar rules that parse the contents of (action ...) as an action, recognizing the various constructs of this DSL.

+

The output of the parser is this syntax tree with location information (for +some reason, line numbers start at 0 which is normal and unusual at the same +time).

+
(source_file [0, 0] - [5, 0]
+  (stanza [0, 0] - [4, 22]
+    (stanza_name [0, 1] - [0, 5])
+    (field_name [1, 2] - [1, 8])
+    (action [2, 2] - [4, 20]
+      (action_name [2, 3] - [2, 17])
+      (file_name_target [3, 3] - [3, 10]
+        (file_name [3, 3] - [3, 10]))
+      (action [4, 3] - [4, 19]
+        (action_name [4, 4] - [4, 8])
+        (quoted_string [4, 9] - [4, 18])))))
+

The various strings are annotated with their type: we have stanza names +(rule), field names (action), action names (with-stdout-to, echo), file +names (foo.txt), and plain strings ("testing").

+

By itself, that is not useful, but it’s possible to write queries to make +this syntax tree do interesting stuff.

+

The first one is highlighting: we can set styles for various “patterns” (in +practice, I only used node names) by defining queries:

+
(stanza_name) @function
+(field_name) @property
+(quoted_string) @string
+(multiline_string) @string
+(action_name) @keyword
+

The parts with @ map to “highlight groups” used in text editors.

+

Another type of query is called “injections”. It is used to link different +types of grammars together. For example, dune files can start with a special +comment that indicates that the rest of the file is an OCaml program. In that +case, the parser emits a single ocaml_syntax node and the following injection +indicates that this file should be parsed using an OCaml parser:

+
((ocaml_syntax) @injection.content
+ (#set! injection.language "ocaml"))
+

Another use case for this is system actions: these strings in dune files +could be interpreted using a shell parser.

+

In the other direction, it is possible to inject dune files into another +document. For example, a markdown parser can use injections to highlight code +blocks.

+

I’m happy to have explored this technology. The toolchain seemed complex at +first: there’s a compiler which seems to be a mix of node and rust, which +generates C, which is compiled into a dynamically loaded library; but this is +actually pretty well integrated in nix and neovim to the details are made +invisible.

+

The testing mechanism is similar to the cram tests we use in Dune, but I was a +bit confused with the colors at first: when the output of a test changes, Dune +considers that the new output is a + in the diff, and highlights it in green; +while tree-sitter considers that the “expected output” is green.

+

There are many ways to improve this prototype: either by adding queries (it’s +possible to define text objects, folding expressions, etc), or by improving +coverage for dune files (in most cases, the parser uses a s-expression +fallback). I’m also curious to see if it’s possible to use this parser to +provide a completion source. Since the strings are tagged with their type (are +we expecting a library name, a module name, etc), I think we could use that to +provide context-specific completions, but that’s probably difficult to do.

+

Thanks teej for the initial idea and the useful +resources.

diff --git a/data/planet/emilpriver/why-i-like-ocaml.md b/data/planet/emilpriver/why-i-like-ocaml.md new file mode 100644 index 0000000000..a92cddd8f1 --- /dev/null +++ b/data/planet/emilpriver/why-i-like-ocaml.md @@ -0,0 +1,374 @@ +--- +title: Why I Like Ocaml +description: I like OCaml and this is why +url: https://priver.dev/blog/ocaml/why-i-like-ocaml/ +date: 2024-07-21T12:10:55-00:00 +preview_image: https://priver.dev/images/ocaml/ocaml-cover.png +authors: +- "Emil Priv\xE9r" +source: +--- + +

According to my Linkedin profile, I have been writing code for a company for almost 6 years. During this time, I have worked on PHP and Wordpress projects, built e-commerce websites using NextJS and JavaScript, written small backends in Python with Django/Flask/Fastapi, and developed fintech systems in GO, among other things. I have come to realize that I value a good type system and prefer writing code in a more functional way rather than using object-oriented programming. For example, in GO, I prefer passing in arguments rather than creating a struct method. This is why I will be discussing OCaml in this article.

+

If you are not familiar with the language OCaml or need a brief overview of it, I recommend reading my post OCaml introduction before continuing with this post. It will help you better understand the topic I am discussing.

+

Hindley-Milner type system and type inference

+

Almost every time I ask someone what they like about OCaml, they often say “oh, the type system is really nice” or “I really like the Hindley-Milner type system.” When I ask new OCaml developers what they like about the language, they often say “This type system is really nice, Typescript’s type system is actually quite garbage.” I am not surprised that these people say this, as I agree 100%. I really enjoy the Hindley-Milner type system and I think this is also the biggest reason why I write in this language. A good type system can make a huge difference for your developer experience.

+

For those who may not be familiar with the Hindley-Milner type system, it can be described as a system where you write a piece of program with strict types, but you are not required to explicitly state the types. Instead, the type is inferred based on how the variable is used. +Let’s look at some code to demonstrate what I mean. In GO, you would be required to define the type of the arguments:

+
+ +
+
1
+2
+3
+4
+5
+
 +
package main
+
+func FirstName(name string) {
+  fmt.Println(name)
+}
+
+
+

However, in OCaml, you don’t need to specify the type:

+
+ +
+
1
+2
+
 +
let first_name name = 
+  print_endline name
+
+
+

Since print_endline expects to receive a string, the signature for hello will be:

+
+ +
+
1
+
 +
val first_name : string -> unit
+
+
+

But it’s not just for arguments, it’s also used when returning a value.

+
+ +
+
1
+2
+3
+4
+
 +
let first_name name = 
+  match name with 
+  | Some value -> "We had a value" 
+  | None -> 1
+
+
+

This function will not compile because we are trying to return a string as the first value and later an integer. +I also want to provide a larger example of the Hindley-Milner type system:

+
+ +
+
 1
+ 2
+ 3
+ 4
+ 5
+ 6
+ 7
+ 8
+ 9
+10
+11
+12
+13
+14
+15
+16
+17
+
 +
module Car = struct
+  type car = {
+    car: string;
+    age: int;
+  }
+
+  let make car_name age = { car = car_name; age }
+
+  let print_car_name car = print_endline car.car
+
+  let print_car_age car = print_int car.age
+end
+
+let () =
+  let car = Car.make "Volvo" 12 in
+  Car.print_car_name car;
+  Car.print_car_age car
+
+
+

The signature for this piece of code will be:

+
+ +
+
1
+2
+3
+4
+5
+6
+7
+
 +
module Car :
+  sig
+    type car = { car : string; age : int; }
+    val make : string -> int -> car
+    val print_car_name : car -> unit
+    val print_car_age : car -> unit
+  end
+
+
+

In this example, we create a new module where we expose 3 functions: make, print_car_age, and print_car_name. We also define a type called car. One thing to note in the code is that the type is only defined once, as OCaml infers the type within the functions since car is a type within this scope.

+

OCaml playground for this code +Something important to note before concluding this section is that you can define both the argument types and return types for your function.

+
+ +
+
1
+2
+3
+
 +
let first_name (name: string) : int = 
+  print_endline name;
+  1
+
+
+

Pattern matching & Variants

+

The next topic is pattern matching. I really enjoy pattern matching in programming languages. I have written a lot of Rust, and pattern matching is something I use when I write Rust. Rich pattern matching is beneficial as it eliminates the need for many if statements. Additionally, in OCaml, you are required to handle every case of the match statement.

+

For example, in the code below:

+
+ +
+
1
+2
+3
+4
+5
+
 +
let first_name name = 
+  match name with 
+  | "Emil" -> print_endline "Hello Emil"
+  | "Sabine the OCaml queen" -> print_endline "Raise your swords soldiers, the queen has arrived"
+  | value -> Printf.printf "Hello stranger %s" value
+
+
+

In the code above, I am required to include the last match case because we have not handled every case. For example, what should the compiler do if the name is Adam? The example above is very simple. We can also match on an integer and perform different actions based on the number value. For instance, we can determine if someone is allowed to enter the party using pattern matching.

+
+ +
+
1
+2
+3
+4
+5
+6
+7
+8
+
 +
let allowed_to_join age =
+  match age with
+  | 0 -> print_endline "Can you even walk lol"
+  | value when value > 18 ->
+    print_endline "Welcome in my friend, the beer is on Sabine"
+  | _ -> print_endline "Your not allowed, go home and play minecraft"
+
+let () = allowed_to_join 2
+
+
+

OCaml playground

+

But the reason I mention variants in this section is that variants and pattern matching go quite nicely hand in hand. A variant is like an enumeration with more features, and I will show you what I mean. We can use them as a basic enumeration, which could look like this:

+
+ +
+
1
+2
+3
+4
+
 +
type person =
+ | Name
+ | Age 
+ | FavoriteProgrammingLanguage
+
+
+

This now means that we can do different things depending on this type:

+
+ +
+
1
+2
+3
+4
+
 +
match person with
+ | Name -> print_endline "John"
+ | Age -> print_endline "30"
+ | FavoriteProgrammingLanguage -> print_endline "OCaml"
+
+
+

But I did mention that variants are similar to enumeration with additional features, allowing for the assignment of a type to the variant.

+
+ +
+
1
+2
+3
+4
+5
+
 +
type person =
+ | Name of string
+ | Age of int
+ | FavoriteProgrammingLanguage of string
+ | HavePets
+
+
+

Now that we have added types to our variants and included HavePets, we are able to adjust our pattern matching as follows:

+
+ +
+
1
+2
+3
+4
+5
+6
+7
+
 +
let () =
+  let person = Name "Emil" in
+  match person with
+   | Name name -> Printf.printf "Name: %s\n" name
+   | Age age -> Printf.printf "Age: %d\n" age
+   | FavoriteProgrammingLanguage language -> Printf.printf "Favorite Programming Language: %s\n" language
+   | HavePets -> Printf.printf "Has pets\n"
+
+
+

OCaml Playground

+

We can now assign a value to the variant and use it in pattern matching to print different values. As you can see, I am not forced to add a value to every variant. For instance, I do not need a type on HavePets so I simply don’t add it. +I often use variants, such as in DBCaml where I use variants to retrieve responses from a database. For example, I return NoRows if I did not receive any rows back, but no error.

+

OCaml also comes with Exhaustiveness Checking, meaning that if we don’t check each case in a pattern matching, we will get an error. For instance, if we forget to add HavePets to the pattern matching, OCaml will throw an error at compile time.

+
+ +
+
1
+2
+3
+4
+5
+6
+7
+8
+
 +
File "bin/main.ml", lines 9-12, characters 2-105:
+ 9 | ..match person with
+10 |    | Name name -> Printf.printf "Name: %s\n" name
+11 |    | Age age -> Printf.printf "Age: %d\n" age
+12 |    | FavoriteProgrammingLanguage language -> Printf.printf "Favorite Programming Language: %s\n" language
+Error (warning 8 [partial-match]): this pattern-matching is not exhaustive.
+Here is an example of a case that is not matched:
+HavePets
+
+
+

Binding operators

+

The next topic is operators and specific binding operators. OCaml has more types of operators, but binding operators are something I use in every project. +A binding could be described as something that extends how let works in OCaml by adding extra logic before storing the value in memory with let. +I’ll show you:

+
+ +
+
1
+
 +
let first_name = "Emil" in 
+
+
+

This code simply takes the value “Emil” and stores it in memory, then assigns the memory reference to the variable hello. However, we can extend this functionality with a binding operator. For instance, if we don’t want to use a lot of match statements on the return value of a function, we can bind let so it checks the value and if the value is an error, it bubbles up the error.

+
+ +
+
 1
+ 2
+ 3
+ 4
+ 5
+ 6
+ 7
+ 8
+ 9
+10
+11
+12
+
 +
let ( let* ) r f = match r with Ok v -> f v | Error _ as e -> e
+
+let check_result =
+  let* hello = Ok "Emil" in
+  let* second_name = Ok "Priver" in
+  let* non_existing = Error "no name" in
+  Ok (hello ^ second_name)
+
+let () =
+  match check_result with
+  | Ok name -> print_endline name
+  | Error _ -> print_endline "no name"
+
+
+

This allows me to reduce the amount of code I write while maintaining the same functionality.

+

In the code above, one of the variables is an Error, which means that the binding will return the error instead of returning the first name and last name.

+

It’s functional on easy mode

+

I really like the concept of functional programming, such as immutability and avoiding side-effects as much as possible. However, I believe that a purely functional programming language could force us to write code in a way that becomes too complex. This is where I think OCaml does a good job. OCaml is clearly designed to be a functional language, but it allows for updating existing values rather than always returning new values.

+
+

Immutability means that you cannot change an already existing value and must create a new value instead. I have written about the Concepts of Functional Programming and recommend reading it if you want to learn more.

+
+

One example where functional programming might make the code more complex is when creating a reader to read some bytes. If we strictly follow the rule of immutability, we would need to return new bytes instead of updating existing ones. This could lead to inefficiencies in terms of memory usage.

+

Just to give an example of how to mutate an existing value in OCaml, I have created an example. In the code below, I am updating the age by 1 as it is the user’s birthday:

+
+ +
+
 1
+ 2
+ 3
+ 4
+ 5
+ 6
+ 7
+ 8
+ 9
+10
+11
+12
+13
+14
+
 +
type user = { mutable age : int; name : string }
+
+let make_user name age = { age; name }
+let increase_age user = user.age <- user.age + 1
+
+let () =
+  let user = make_user "Emil" 25 in
+  Printf.printf "It's %s's birthday today! Congratz!!!!" user.name;
+  print_newline ();
+  print_int user.age;
+  print_newline ();
+  increase_age user;
+  print_int user.age;
+  print_newline ()
+
+
+

What I mean by “it’s functional on easy mode” is simply that the language is designed to be a functional language, but you are not forced to strictly adhere to functional programming rules.

+

The end

+

It is clear to me that a good type system can greatly improve the developer experience. I particularly appreciate OCaml’s type system, as well as its option and result types, which I use frequently. In languages like Haskell, you can extend the type system significantly, to the point where you can write an entire application using only types. However, I believe that this can lead to overly complex code. This is another aspect of OCaml that I appreciate - it has a strong type system, but there are limitations on how far you can extend it.

+

I hope you enjoyed this article. If you are interested in joining a community of people who also enjoy functional programming, I recommend joining this Discord server.

+ diff --git a/data/planet/frama-c/beta-release-of-frama-c-300beta-zinc.md b/data/planet/frama-c/beta-release-of-frama-c-300beta-zinc.md new file mode 100644 index 0000000000..3209247c22 --- /dev/null +++ b/data/planet/frama-c/beta-release-of-frama-c-300beta-zinc.md @@ -0,0 +1,12 @@ +--- +title: Beta release of Frama-C 30.0~beta (Zinc) +description: +url: https://frama-c.com/fc-versions/zinc.html +date: 2024-11-07T00:00:00-00:00 +preview_image: +authors: +- Frama-C +source: +--- + + diff --git a/data/planet/frama-c/frama-clang-v0016-for-frama-c-290-copper.md b/data/planet/frama-c/frama-clang-v0016-for-frama-c-290-copper.md new file mode 100644 index 0000000000..57390619c3 --- /dev/null +++ b/data/planet/frama-c/frama-clang-v0016-for-frama-c-290-copper.md @@ -0,0 +1,12 @@ +--- +title: Frama-Clang v0.0.16 for Frama-C 29.0 Copper +description: +url: https://frama-c.com/html/news.html#2024-09-05 +date: 2024-09-05T00:00:00-00:00 +preview_image: +authors: +- Frama-C +source: +--- + + diff --git a/data/planet/frama-c/metacsl-v07-for-frama-c-290-copper.md b/data/planet/frama-c/metacsl-v07-for-frama-c-290-copper.md new file mode 100644 index 0000000000..00879b44c1 --- /dev/null +++ b/data/planet/frama-c/metacsl-v07-for-frama-c-290-copper.md @@ -0,0 +1,12 @@ +--- +title: MetAcsl v0.7 for Frama-C 29.0~ Copper +description: +url: https://frama-c.com/fc-plugins/metacsl.html +date: 2024-10-03T00:00:00-00:00 +preview_image: +authors: +- Frama-C +source: +--- + + diff --git a/data/planet/frama-c/the-guide-to-software-verification-with-frama-c-is-available.md b/data/planet/frama-c/the-guide-to-software-verification-with-frama-c-is-available.md new file mode 100644 index 0000000000..a05cb681a4 --- /dev/null +++ b/data/planet/frama-c/the-guide-to-software-verification-with-frama-c-is-available.md @@ -0,0 +1,12 @@ +--- +title: The Guide to Software Verification with Frama-C is available +description: +url: https://link.springer.com/book/10.1007/978-3-031-55608-1 +date: 2024-08-08T00:00:00-00:00 +preview_image: https://media.springernature.com/w153/springer-static/cover/book/978-3-031-55608-1.jpg +authors: +- Frama-C +source: +--- + + diff --git a/data/planet/frama-c/the-slides-presented-at-frama-c-days-2024-are-available.md b/data/planet/frama-c/the-slides-presented-at-frama-c-days-2024-are-available.md new file mode 100644 index 0000000000..cce22888e6 --- /dev/null +++ b/data/planet/frama-c/the-slides-presented-at-frama-c-days-2024-are-available.md @@ -0,0 +1,12 @@ +--- +title: The slides presented at Frama-C Days 2024 are available +description: +url: https://frama-c.com/html/publications/frama-c-days-2024/index.html +date: 2024-08-05T00:00:00-00:00 +preview_image: +authors: +- Frama-C +source: +--- + + diff --git a/data/planet/janestreet/developer-education-at-jane-street.md b/data/planet/janestreet/developer-education-at-jane-street.md new file mode 100644 index 0000000000..5621d742bf --- /dev/null +++ b/data/planet/janestreet/developer-education-at-jane-street.md @@ -0,0 +1,20 @@ +--- +title: Developer education at Jane Street +description: Like most places, Jane Street largely teaches developers through a kind + of apprenticeshipmodel. A team matching process tries to thoughtfully match new + devs ... +url: https://blog.janestreet.com/developer-education-at-jane-street-index/ +date: 2024-10-04T00:00:00-00:00 +preview_image: https://blog.janestreet.com/developer-education-at-jane-street-index/classroom.png +authors: +- Jane Street Tech Blog +source: +--- + +

Like most places, Jane Street largely teaches developers through a kind of apprenticeship +model. A team matching process tries to thoughtfully match new devs to a team that suits +them; and from there carefully chosen projects, one-on-one mentorship, code review, and +close collaboration with people “on the row” – teammates sitting near you – does most of +the rest.

+ + diff --git a/data/planet/janestreet/icfp-2024.md b/data/planet/janestreet/icfp-2024.md new file mode 100644 index 0000000000..1f1b48ea72 --- /dev/null +++ b/data/planet/janestreet/icfp-2024.md @@ -0,0 +1,22 @@ +--- +title: ICFP 2024 +description: "It\u2019s no secret that Jane Street is an active participant in the + programming languagecommunity, and we\u2019re excited to be attending ICFP 2024, + theInternational ..." +url: https://blog.janestreet.com/icfp-2024-index/ +date: 2024-08-29T00:00:00-00:00 +preview_image: https://blog.janestreet.com/icfp-2024-index/ICFP-2024.png +authors: +- Jane Street Tech Blog +source: +--- + +

It’s no secret that Jane Street is an active participant in the programming language +community, and we’re excited to be attending ICFP 2024, the +International Conference on Functional Programming, in Milan next week! Most members of +our OCaml Language team will be there, and as usual, we look forward to sharing our work +with the wider community. Please see below for a full list of papers and talks that Jane +Street folk are involved in. Note that a lot of these are collaborations of one kind or +another with researchers outside of Jane Street.

+ + diff --git a/data/planet/janestreet/visualizing-piecewise-linear-neural-networks.md b/data/planet/janestreet/visualizing-piecewise-linear-neural-networks.md new file mode 100644 index 0000000000..acc96718c5 --- /dev/null +++ b/data/planet/janestreet/visualizing-piecewise-linear-neural-networks.md @@ -0,0 +1,15 @@ +--- +title: Visualizing piecewise linear neural networks +description: Neural networks are often thought of as opaque, black-box function approximators, + but theoretical tools let us describe and visualize their behavior. In part... +url: https://blog.janestreet.com/visualizing-piecewise-linear-neural-networks/ +date: 2024-07-22T00:00:00-00:00 +preview_image: https://blog.janestreet.com/visualizing-piecewise-linear-neural-networks/./6_1.png +authors: +- Jane Street Tech Blog +source: +--- + +

Neural networks are often thought of as opaque, black-box function approximators, but theoretical tools let us describe and visualize their behavior. In particular, let’s study piecewise-linearity, a property many neural networks share. This property has been studied before, but we’ll try to visualize it in more detail than has been previously done. 

+ + diff --git a/data/planet/janestreet/what-the-interns-have-wrought-2024-edition.md b/data/planet/janestreet/what-the-interns-have-wrought-2024-edition.md new file mode 100644 index 0000000000..bafae3c3e3 --- /dev/null +++ b/data/planet/janestreet/what-the-interns-have-wrought-2024-edition.md @@ -0,0 +1,16 @@ +--- +title: What the interns have wrought, 2024 edition +description: "We\u2019re once again at the end of our internship season, and it\u2019s + time do our annual reviewof what the interns achieved while they were here." +url: https://blog.janestreet.com/what-the-interns-have-wrought-2024-edition-index/ +date: 2024-08-26T00:00:00-00:00 +preview_image: https://blog.janestreet.com/what-the-interns-have-wrought-2024-edition-index/WTIHW-2024.png +authors: +- Jane Street Tech Blog +source: +--- + +

We’re once again at the end of our internship season, and it’s time do our annual review +of what the interns achieved while they were here.

+ + diff --git a/data/planet/ocamlpro/alt-ergo-26-is-out.md b/data/planet/ocamlpro/alt-ergo-26-is-out.md new file mode 100644 index 0000000000..eabc5f0ab9 --- /dev/null +++ b/data/planet/ocamlpro/alt-ergo-26-is-out.md @@ -0,0 +1,246 @@ +--- +title: Alt-Ergo 2.6 is Out! +description: We are excited to announce the release of Alt-Ergo 2.6! Alt-Ergo is an + open-source automated prover used for formal verification in software development. + It is part of the arsenal behind static analysis frameworks such as TrustInSoft + Analyzer and Frama-C, and is one of the solvers behind Why3, a pla... +url: https://ocamlpro.com/blog/2024_09_01_alt_ergo_2_6_0_released +date: 2024-09-30T16:50:25-00:00 +preview_image: https://ocamlpro.com/blog/assets/img/alt-ergo-8-colors.png +authors: +- "\n Basile Cl\xE9ment\n " +source: +--- + +

+

+

+

+ + The Alt-Ergo 2.6 release comes with many enhancements! + +

+ The Alt-Ergo 2.6 release comes with many enhancements! +
+ +
+ +

We are excited to announce the release of Alt-Ergo 2.6!

+

Alt-Ergo is an open-source automated prover used for formal verification in +software development. It is part of the arsenal behind static analysis +frameworks such as TrustInSoft Analyzer and Frama-C, and is one of the +solvers behind Why3, a platform for deductive program verification. The newly +released version 2.6 brings new features and performance improvements.

+

Development on Alt-Ergo has accelerated significantly this past year, thanks to +the launch of the DéCySif joint research project (i-Démo) +with AdaCore, Inria, OCamlPro and TrustInSoft. The improvements to bit-vectors +and algebraic data types in this release are sponsored by the Décysif project.

+

The highlights of Alt-Ergo 2.6 are:

+ +

Alt-Ergo 2.6 also includes other improvements to the user interface (notably +the set-option SMT-LIB command), use of Dolmen as the default frontend for +SMT-LIB and native input, and many bug fixes.

+

Bit-vectors

+

In Alt-Ergo 2.5, we introduced built-in functions for the bit-vector +primitives from the SMT-LIB standard, but only provided limited reasoning +support. For Alt-Ergo 2.6, we set out to improve this reasoning support, and +have developed a new and improved relational theory for bit-vectors. This new +theory is based on an also new constraint propagation core that draws heavily +on the architecture of the Colibri solver (as in Sharpening Constraint +Programming approaches for Bit-Vector Theory), integrated into Alt-Ergo's +existing normalizing Shostak solver.

+

Bit-vectors are commonly used in verification of low-level code and in +cryptography, so improved support significantly enhances Alt-Ergo’s +applicability in these domains.

+

There are still areas of improvements, so please share any issue you encounter +with the bit-vector theory (or Alt-Ergo in general) via our +issue tracker.

+

To showcase improvements in Alt-Ergo 2.6, we compared it against the version +2.5 and industry-leading solvers Z3 and CVC5 on a dataset of bit-vector +problems collected from our partners in the DéCySif project. The (no BV) +variants for Alt-Ergo do not use the new bit-vector theory but instead an +axiomatization of bit-vector primitives provided by Why3. The percentages +represent the proportion of bit-vector problems solved successfully in each +configuration.

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
AE 2.5AE 2.6Z3 (4.12.5)CVC5 (1.1.2)Total
(BV)(no BV)(BV)(no BV)
#4128487062654940548274159038
%46%54%69%54%61%82%100%
+

As the table shows, Alt-Ergo 2.6 significantly outperforms version 2.5, and the +new built-in bit-vector theory outperforms Why3's axiomatization. We even +surpass Z3 on this benchmark, a testament to the new bit-vector theory in +Alt-Ergo 2.6.

+

Model Generation

+

Bit-vector is not the only theory Alt-Ergo 2.6 improves upon. Model generation +was introduced in Alt-Ergo 2.5 with support for booleans, integers, reals, +arrays, enumerated types, and records. Alt-Ergo 2.6 extends this support to +bit-vector and arbitrary algebraic data types, which means that model +generation is now enabled for all the theories supported by Alt-Ergo.

+

Model generation allows users to extract concrete examples or counterexamples, +aiding in debugging and verification of their systems.

+

Model generation is also more robust in Alt-Ergo 2.6, with numerous bug fixes +and improvements for edge cases.

+

Optimization

+

Alt-Ergo 2.6 introduces optimization capabilities, available via SMT-LIB input +using OptiSMT primitives such as (minimize) and (maximize) and compatible +with Z3 and OptiMathSat. Optimization allows guiding the solver towards simpler +and smaller counterexamples, helping users find more concrete and realistic +scenarios to trigger a bug.

+

See some +examples in the +documentation.

+

SMT-LIB command support

+

Alt-Ergo 2.6 supports more SMT-LIB syntax and commands, such as:

+ +

See the SMT-LIB standard for more details about these +commands.

+

Floating-point theory

+

In this release, we have made Alt-Ergo's floating-point +theory +enabled by default: there is no need to provide the --enable-theories fpa +flag anymore. The theory can be disabled with --disable-theories fpa,nra,ria +(the nra and ria theories were automatically enabled along with the fpa +theory in Alt-Ergo 2.5).

+

We have also made the floating-point primitives available in the SMT-LIB +format as the indexed constant ae.round and the convenience ae.float16, +ae.float32, ae.float64 and ae.float128 functions; see the +documentation.

+

Dolmen is the new default frontend

+

Introduced in Alt-Ergo 2.5, the Dolmen frontend has been rigorously tested for +regressions and is now the default for both .smt2 and .ae files; the +--frontend dolmen flag that was introduced in Alt-Ergo 2.5 is no longer +necessary.

+

The Dolmen frontend is based on the Dolmen +library developed by Guillaume Bury at OCamlPro. It provides excellent support +for the SMT-LIB standard and is used to check validity of all new problems in +the SMT-LIB benchmark collection, as well as the results of the annual SMT-LIB +affiliated solver competition SMT-COMP.

+

The preferred input format for Alt-Ergo is now the SMT-LIB format. The legacy +.ae format is still supported, but is now deprecated and users are +encouraged to migrate to the SMT-LIB format if possible. Please reach +out if you find any issue while migrating to +the SMT-LIB format.

+

As we announced when releasing Alt-Ergo 2.5, the legacy frontend (supports +.ae files only) is deprecated in Alt-Ergo 2.6, but it can still be +enabled with the --frontend legacy option. It will be removed entirely from +Alt-Ergo 2.7.

+

Parser extensions, such as the built-in AB-Why3 plugin, only work with the +legacy frontend, and will no longer work with Alt-Ergo 2.7. We are not +aware of any current users of either parser extensions or the AB-Why3 plugin: +if you need these features, please reach out to us on +GitHub or by +email so that we can figure out a path +forward.

+

Use of dune-site for plugins

+

Starting with Alt-Ergo 2.6, we are using the plugin mechanism from +dune-site to replace the custom plugin loading Dynlink. Plugins now need +to be registered in the (alt-ergo plugins) site with the +plugin stanza.

+

This does not impact users, but only impacts developers of Alt-Ergo plugins. See the +dune file +for Alt-Ergo's built-in FM-Simplex plugin for reference.

+

Binary releases on GitHub

+

Starting with Alt-Ergo 2.6, we will be providing binary releases on the +GitHub Releases page for +Linux (x86_64) and macOS (x86_64 and arm). These are released under the +same licensing conditions as the Alt-Ergo source code.

+

The binary releases are statically linked and have no dependencies, except +for system dependencies on macOS. They do not support dynamically loading +plugins.

+

Performance

+

For Alt-Ergo 2.6, our main focus of improvement in term of reasoning was on +bit-vectors and algebraic data types. Other theories also benefit from +broader performance improvements we made. On our internal +problem dataset, Alt-Ergo 2.6 is about 5% faster than Alt-Ergo 2.5 on the goals +they both prove.

+

And more!

+

This release also includes significant internal refactoring, notably +a rewrite from scratch of the interval domain. This improves the +accuracy of Alt-Ergo in handling interval arithmetic and facilitates mixed +operations involving integers and bit-vectors, resulting in shorter and more +reliable proofs.

+

See the complete changelog +here.

+

We encourage you to try out Alt-Ergo 2.6 and share your experience or any +feedback on our GitHub or by email at +alt-ergo@ocamlpro.com. Your input will help +share future releases!

+

Acknowledgements

+

We thank the Alt-Ergo Users' Club members: AdaCore, the CEA, Thales, +Mitsubishi Electric R&D Center Europe (MERCE) and TrustInSoft.

+

Special thanks to David Mentré and Denis Cousineau at MERCE for funding the +initial optimization work. MERCE has been a Member of the Alt-Ergo Users' +Club for four years. This partnership allowed Alt-Ergo to evolve and we hope +that more users will join the Club on our journey to make Alt-Ergo a must-have +tool.

+
+
+ AdaCore logo + CEA list logo + Thales logo + Mitsubishi Electric logo + TrustInSoft logo +
+
The dedicated members of our Alt-Ergo Club!
+
+ diff --git a/data/planet/ocamlpro/flambda2-ep-3-speculative-inlining-.md b/data/planet/ocamlpro/flambda2-ep-3-speculative-inlining-.md new file mode 100644 index 0000000000..7c6404e8c7 --- /dev/null +++ b/data/planet/ocamlpro/flambda2-ep-3-speculative-inlining-.md @@ -0,0 +1,472 @@ +--- +title: 'Flambda2 Ep. 3: Speculative Inlining ' +description: 'Welcome to a new episode of The Flambda2 Snippets! The F2S blog posts + aim at gradually introducing the world to the inner-workings of a complex piece + of software engineering: The Flambda2 Optimising Compiler for OCaml, a technical + marvel born from a 10 year-long effort in Research & Development and ...' +url: https://ocamlpro.com/blog/2024_08_09_the_flambda2_snippets_3 +date: 2024-08-09T16:50:25-00:00 +preview_image: https://www.ocamlpro.com/blog/assets/img/picture_egyptian_weighing_of_heart.jpg +authors: +- "\n Pierre Chambart\n " +source: +--- + +

+

+

+

+ + A representation of Speculative Inlining through the famous Weighing Of The Heart of Egyptian Mythology. Egyptian God Anubis weighs his OCaml function, to see if it is worth inlining.<br />Credit: The Weighing of the Heart Ceremony, Ammit. Angus McBride (British, 1931-2007) + +

+ A representation of Speculative Inlining through the famous Weighing Of The Heart of Egyptian Mythology. Egyptian God Anubis weighs his OCaml function, to see if it is worth inlining.
Credit: The Weighing of the Heart Ceremony, Ammit. Angus McBride (British, 1931-2007) +
+ +
+ +

Welcome to a new episode of The Flambda2 Snippets!

+
+

The F2S blog posts aim at gradually introducing the world to the +inner-workings of a complex piece of software engineering: The Flambda2 Optimising Compiler for OCaml, a technical marvel born from a 10 year-long +effort in Research & Development and Compilation; with many more years of +expertise in all aspects of Computer Science and Formal Methods.

+
+

Today's article will serve as an introduction to one of the key design +decisions structuring Flambda2 that we will cover in the next episode in the +series: Upward and Downward Traversals.

+

See, there are interesting things to be said about how inlining is conducted +inside of our compiler. Inlining in itself is rather ubiquitous in compilers. +The goal here is to show how we approach inlining, and present what we call +Speculative Inlining.

+

+Table of contents + +

+

+Inlining in general +

+

Given the way people write functional programs, inlining is an important part +of the optimisation pipeline of such functional langages.

+

What we call inlining in this series is the process of duplicating some +code to specialise it to a specific context.

+

Usually, this can be thought as copy-pasting the body of a function at its +call site. A common misunderstanding is to think that the main benefit of this +optimisation is to remove the cost of the function call. However, with modern +computer architectures, this has become less and less relevant in the last +decades. The actual benefit is to use the specific context to trigger further +optimisations.

+

Suppose we have the following option_map and double functions:

+
let option_map f x =
+  match x with
+  | None -> None
+  | Some x -> Some (f x)
+
+let double i =
+  i + i
+
+

Additionally, suppose we are currently considering the following function:

+
let stuff () =
+  option_map double (Some 21)
+
+

In this short example, inlining the option_map function would perform the +following transformation:

+
let stuff () =
+  let f = double in
+  let x = Some 21 in
+  match x with
+  | None -> None
+  | Some x -> Some (f x)
+
+

Now we can inline the double function.

+
let stuff () =
+  let x = Some 21 in
+  match x with
+  | None -> None
+  | Some x ->
+    Some (let i = x in i + i)
+
+

As you can see, inlining alone isn't that useful of an optimisation per se. In +this context, appliquing Constant Propagation will optimise and simplify it +to the following:

+
let stuff () = Some 42
+
+

Although this is a toy example, combining small functions is a common pattern +in functional programs. It's very convenient that using combinators is not +significantly worse than writing this function by hand.

+

+When inlining is detrimental +

+

We cannot just go around and inline everything, everywhere... all at once.

+

As we said, inlining is mainly code duplication and that would be +detrimental and blow the size of the compiled code drastically. However, there +is a sweet spot to be found, between both absolute inlining and no inlining at +all, but it is hard to find.

+

Here's an example of exploding code at inlining time:

+
(* val h : int -> int *)
+let h n = (* Some non constant expression *)
+
+(* val f : (int -> int) -> int -> int *)
+let f g x = g (g x)
+
+(* 4 calls to f -> 2^4 calls to h *)
+let n = f (f (f (f h))) 42
+
+

Following through with the inlining process will produce a very large binary +relative to its source code. This contrived example highlights potential +problems that might arise in ordinary codebases in the wild, even if this one +is tailored to be quite nasty for inlining: notice the exponential blowup +in the number of nested calls, every additional call to f doubles the number +of calls to h after inlining.

+

+How to decide when inlining is beneficial +

+

Most compilers use a collection of heuristics to guide them in the decision +making. A good collection of heuristics is hard to both design, and fine-tune. +They also can be quite specific to a programming style and unfit for other +compilers to integrate. The take away is: there is no best way.

+
+

Side Note:

+

This topic would make for an interesting blog post but, +unfortunately, rather remote from the point of this article. If you are +interested in going deeper into that subject right now, we have found +references for you to explore until we get around to writing a comprehensive, +and more digestable, explanation about the heuristic nature of inlining:

+ +
+

Before we get to a concrete example, and break down Speculative Inlining for +you, we would like to discuss the trade-offs of duplicating code.

+

CPUs execute instructions one by one, or at least they pretend that they do. In +order to execute an instruction, they need to load up into memory both code and +data. In modern CPUs, most instructions take only a few cycles to execute and +in practice, the CPUs often execute several at the same time. To put into +perspective, loading memory, however, in the worst case, can take hundreds of +CPU cycles... Most of the time it's not the case because CPUs have complex +memory cache hierarchies such that loading from instruction cache can take just +a few cycles, loading from level 2 caches may take dozens of them, and the +worst case is loading from main memory which can take hundreds of cycles.

+

The take away is, when executing a program, the cost of one instruction +that has to be loaded from main memory can be +larger than the cost of executing a +hundred instructions in caches.

+

There is a way to avoid the worst case scenario. Since caches are rather small +in size, the main component to keeping from loading from main memory is to keep +your program rather small, or at least the parts of it that are regularly +executed.

+

Keep these orders of magnitude in mind when we address the trade-offs between +improving the number of instructions that we run and keeping the program to a +reasonably small size.

+
+

Before explaining Speculative Inlining let's consider a piece of code.

+

The following pattern is quite common in OCaml and other functional languages, +let's see how one would go about inlining this code snippet.

+

Example 1: Notice the higher-order function f:

+
(*
+  val f :
+    (condition:bool -> int -> unit) 
+    -> condition:bool
+    -> int
+    -> unit
+ *)
+let f g ~condition n =
+  for i = 0 to n do
+    g ~condition i
+  done
+
+let g_real ~condition i =
+  if condition then
+    (* small operation *)
+  else
+    (* big piece of code *)
+
+let condition = true
+
+let foo n =
+  f g_real ~condition n
+
+

Even for such a small example we will see that the heuristics involved to finding +the right solution can become quite complex.

+

Keeping in mind the fact that condition is always true, the best set of +inlining decisions would yield the following code:

+
(* All the code before [foo] is kept as is, from the previous codeblock *)
+let foo x = 
+  for i = 0 to x do
+    (* small operation *)
+  done
+
+

But if condition had been always false, instead of small operation, we +would have had a big chunk of g_real duplicated in foo (i.e: (* big piece of code *)). Moreover it would +have only spared us the running time of a few call instructions. Therefore, +we would have probably preferred to have kept ourselves from inlining anything.

+

Specifically, we would have liked to have stopped from inlining g, as well as +to have avoided inlining f because it would have needlessly increased the +size of the code with no substantial benefit.

+

However, if we want to be able to take an educated decision based on the value +of condition, we will have to consider the entirety of the code relevant to +that choice. Indeed, if we just look at the code for f, or its call site in +foo, nothing would guide us to the right decision. In order to take the +right decision, we need to understand that if the ~condition parameter to the +g_real function is true, then we can remove a large piece of code, +namely: the else branch and the condition check as well.

+

But to understand that the ~condition in g_real is always true, we need +to see it in the context of f in foo. This implies again that, that choice +of inlining is not based on a property of g_real but rather a property of the +context of its call.

+

There exists a very large number of combinations of such difficult +situations that would each require different heuristics which would be +incredibly tedious to design, implement, and maintain.

+

+Speculative inlining +

+

We manage to circumvent the hurdle that this decision problem represents +thanks to what we call Speculative Inlining. This strategy requires two +properties from the compiler: the ability to inline and optimise at the same +time, as well as being able to backtrack inlining decisions.

+

Lets look at Example 1 again and look into the Speculative Inlining +strategy.

+
let f g ~condition n =
+  for i = 0 to n do
+    g ~condition i
+  done
+
+let g_real ~condition x =
+  if condition then
+    (* small operation *)
+  else
+    (* big piece of code *)
+
+let condition = true
+
+let foo x =
+  f g_real ~condition x
+
+

We will focus only on the traversal of the foo function.

+

Before we try and inline anything, there are a couple things we have to keep in +mind about values and functions in OCaml:

+
    +
  1. Application arity may not match function arity +
    2. +
+

To give you an idea, the function foo could also been written in the +following way:

+
let foo x =
+  let f1 = f in
+  let f2 = f1 g_real in 
+  let f3 = f2 ~condition in
+  f3 x
+
+

We expect the compiler to translate it as well as the original, but we cannot +inline a function unless all its arguments are provided. To solve this, we need +to handle partial applications precisely. Over-applications also present +similar challenges.

+
    +
  1. Functions are values in OCaml +
    2. +
+

We have to understand that the call to f in foo is not trivially a +direct call to f in this context. Indeed, at this point functions could +instead be stored in pairs, or lists, or even hashtables, to be later retrieved +and applied at will, and we call such functions general functions.

+

Since our goal is to inline it, we need to know the body of the function. We +call a function concrete when we have knowledge of its body. This entails +Constant Propagation +in order to associate a concrete function to general function values and, +consequently, be able to simplify it while inlining.

+

Here's the simplest case to demonstrate the importance of Constant Propagation.

+
let foo_bar y =
+  let pair = foo, y in
+  (fst pair) (snd pair)
+
+

In this case, we have to look inside the pair in order to find the function, +this demonstrates that we sometimes have to do some amount of value analysis in +order to proceed. It's quite common to come across such cases in OCaml programs +due to the module system and other functional languages present similar +characteristics.

+

There are many scenarios which also require a decent amount of context in order +to identify which function should be called. For example, when a function +passed as parameter is called, we need to know the context of the caller +functions, sometimes up to an arbitrarily large context. Analysing the +relevant context will tell us which function is being called and thus help +us make educated inlining decisions. This problem is specific to functional +languages, functions in good old imperative languages are seldom ambiguous; +even though such considerations would be relevant when function pointers are +involved.

+

This small code snippet shows us that we have to inline some functions in +order to know whether we should have inlined them.

+

+Speculative inlining in practice +

+

In practice, Speculative Inlining is being able to quantify the benefits +brought by a set of optimisations, which have to be applied after a given +inlining decision, and use these results to determine if said inlining decision +is in fact worth to carry out all things considered.

+

The criteria for accepting an inlining decision is that the resulting code +should be faster that the original one. We use "should be" because +program speed cannot be fully understood with absolutes.

+

That's why we use a heuristic algorithm in order to compare the original and +the optimised versions of the code. It roughly consists in counting the number +of retired (executed) instructions and comparing it to the increase in code +size introduced by inlining the body of that function. The value of that +cut-off ratio is by definition heuristic and different compilation options +given to ocamlopt change it.

+

As said previously, we cannot go around and evaluate each inlining decision +independently because there are cases where inlining a function allows for more +of them to happen, and sometimes a given inlining choice validates another one. +We can see this in Example 1, where deciding not to inline function +g_real would make the inlining of function f useless.

+

Naturally, every combination of inlining decision cannot be explored +exhaustively. We can only explore a small subset of them, and for that we have +another heuristic that was already used in Flambda1, although Flambda2 does +not yet implement it in full.

+

It's quite simple: we choose to consider inlining decision relationships only +when there are nested calls. As for any other heuristic, it does not cover +every useful case, but not only is it the easiest to implement, we are also +fairly confident that it covers the most important cases.

+

Here's a small rundown of that heuristic:

+ +

Keep in mind that case 2.b is recursive and can go arbitrarily deep. This +amounts to looking for the best leaf in the decision tree. Since we can't +explore the whole tree, we do have a some limit to the depth of the +exploration.

+
+

Reminder for our fellow Cameleers: Flambda1 and Flambda2 have a flag +you can pass through the CLI which will generate a .org file which will +detail all the inlining decisions taken by the compiler. That flag is: +-inlining-report. Note that .org files allow to easily visualise a +decision tree inside of the Emacs editor.

+
+

+Summary +

+

By now, you should have a better understanding of the intricacies inherent to +Speculative Inlining. Prior to its initial inception, it was fair to question +how feasible (and eligible, considering the many requirements for developping a +compiler), such an algorithm would be in practice. Since then, it has +demonstrated its usefulness in Flambda1 and, consequently, its porting to +Flambda2 was called for.

+

So before we move on to the next stop in the +F2S series, lets +summarize what we know of Speculative Inlining.

+

We learned that inlining is the process of copying the body of a function at +its callsite. We also learned that it is not a very interesting transformation by +itself, especially nowadays with how efficient modern CPUs are, but that its +usefulness is found in how it facilitates other optimisations to take place +later.

+

We also learned about the heuristic nature of inlining and how it would be +difficult to maintain finely-tailored heuristics in the long run as many others +have tried before us. Actually, it is because there is no best way that we +have come up with the need for an algorithm that is capable of simultaneously +performing inlining and optimising as well as backtracking when needed +which we called Speculative Inlining. In a nutshell, Speculative Inlining +is one of the algorithms of the optimisation framework of Flambda2 which +facilitates other optimisations to take place.

+

We have covered the constraints that the algorithm has to respect for it to +hold ground in practice, like performance. We value a fast compiler and aim +to keep both its execution but also the code it generates to be so. Take an +optimisation such as Constant Propagation as an example. +It would be a naïve approach to try and perform this transformation +everywhere because the resulting complexity of the compiler would amount to +something like size_of_the_code * number_of_inlinings_performed which is +unacceptable to say the least. We aim at making the complexity of our compiler +linear to the code size, which in turn entails plenty of logarithms anytime +it is possible. Instead, we choose to apply any transformation only in the +inlined parts of the code.

+

With all these parameters in mind, can we imagine ways to tackle these +multi-layered challenges all at the same time ? There are solutions out there +that do so in an imperative manner. In fact, the most intuitive way to +implement such an algorithm may be fairly easily done with imperative code. You +may want to read about Equality Saturation for instance, or even download +Manuel Serrano's Paper inside the Scheme Bigloo +compiler +to learn more about it. However, we require backtracking, and the nested +nature of these transformations (inlining, followed by different optimising +transformations) would make backtracking bug-prone and tedious to +maintain if it was to be written imperatively.

+

It soon became evident for us that we were going to leverage one of the key +characteristics of functional languages in order to make this whole ordeal +easier to design, implement and maintain: purity of terms. Indeed, not only is +it easier to support backtracking when manipulating pure code, but it also +becomes impossible for us to introduce cascades of hard to detect nested +bugs by avoiding transforming code in place. From this point on, we knew we +had to perform all transformations at the same time, making our inlining +function one that would return an optimised inlined function. This does +introduce complexities that we have chosen over the hurdles of maintaining an +imperative version of that same algorithm, which can be seen as pertaining to +graph traversal and tree rewriting for all intents and purposes.

+

Despite the density of this article, keep in mind that we aim at explaining +Flambda2 in the most comprehensive manner possible and that there are +voluntary shortcuts taken throughout these snippets for all of this to make +sense for the broader audience. +In time, these articles will go deep into the guts of the compiler and by then, +hopefully, we will have done a good job at providing our readers with all +necessary information for all of you to continue enjoying this rabbit-hole with +us!

+

Here's a pseudo-code snippet representing Speculative Inlining.

+
(* Pseudo-code to rpz the actual speculation *)
+let try_inlining f env args =
+  let inlined_version_of_f = inline f env args in
+  let benefit = compare inlined_version_of_f f in
+  if benefit > 0 then
+    inlined_version_of_f
+  else
+    f
+
+

+Conclusion +

+

As we said at the start of this article, this one is but an introduction to a +major topic we will cover next, namely: Upwards and Downwards Traversals.

+

We had to cover Speculative Inlining first. It is a reasonably approachable +solution to a complex problem, and having an idea of all the requirements for +its good implementation is half of the work done for understanding key design +decisions such as how code traversal was designed for algorithms such as +Speculative Inlining to hold out.

+
+

Thank you all for reading! We hope that these articles will keep the +community hungry for more!

+

Until next time, keep calm and OCaml! +⚱️🐫🏺📜

+ diff --git a/data/planet/ocamlpro/opam-220-release.md b/data/planet/ocamlpro/opam-220-release.md new file mode 100644 index 0000000000..7bed2a758c --- /dev/null +++ b/data/planet/ocamlpro/opam-220-release.md @@ -0,0 +1,246 @@ +--- +title: opam 2.2.0 release! +description: 'Feedback on this post is welcomed on Discuss! We are very pleased to + announce the release of opam 2.2.0, and encourage all users to upgrade. Please read + on for installation and upgrade instructions. NOTE: this article is cross-posted + on opam.ocaml.org and ocamlpro.com, and published in discuss.ocaml...' +url: https://ocamlpro.com/blog/2024_07_01_opam_2_2_0_releases +date: 2024-07-01T16:50:25-00:00 +preview_image: https://ocamlpro.com/assets/img/og_image_ocp_the_art_of_prog.png +authors: +- "\n Raja Boujbel - OCamlPro\n " +source: +--- + +

Feedback on this post is welcomed on Discuss!

+

We are very pleased to announce the release of opam 2.2.0, and encourage all users to upgrade. Please read on for installation and upgrade instructions.

+
+

NOTE: this article is cross-posted on opam.ocaml.org and ocamlpro.com, and published in discuss.ocaml.org.

+
+

Try it!

+

In case you plan a possible rollback, you may want to first backup your +~/.opam or $env:LOCALAPPDATAopam directory.

+

The upgrade instructions are unchanged:

+
    +
  1. Either from binaries: run +
    2. +
+

For Unix systems

+
bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) --version 2.2.0"
+
+

or from PowerShell for Windows systems

+
Invoke-Expression "& { $(Invoke-RestMethod https://raw.githubusercontent.com/ocaml/opam/master/shell/install.ps1) }"
+
+

or download manually from the Github "Releases" page to your PATH.

+
    +
  1. Or from source, manually: see the instructions in the README. +
    2. +
+

You should then run:

+
opam init --reinit -ni
+
+

Changes

+

Major change: Windows support

+

After 8 years' effort, opam and opam-repository now have official native Windows +support! A big thank you is due to Andreas Hauptmann (@fdopen), +whose WODI and OCaml for Windows +projects were for many years the principal downstream way to obtain OCaml on +Windows, Jun Furuse (@camlspotter) whose +initial experimentation with OPAM from Cygwin +formed the basis of opam-repository-mingw, and, most recently, +Jonah Beckford (@jonahbeckford) whose +DkML distribution kept - and keeps - a full +development experience for OCaml available on Windows.

+

OCaml when used on native Windows requires certain tools from the Unix world +which are provided by either Cygwin or MSYS2. +We have engineered opam init so that it is possible for a user not to need to +worry about this, with opam managing the Unix world, and the user being able +to use OCaml from either the Command Prompt or PowerShell. However, for the Unix +user coming over to Windows to test their software, it is also possible to have +your own Cygwin/MSYS2 installation and use native Windows opam from that. Please +see the previous blog post +for more information.

+

There are two "ports" of OCaml on native Windows, referred to by the name of +provider of the C compiler. The mingw-w64 port is GCC-based. +opam's external dependency (depext) system works for this port (including +providing GCC itself), and many packages are already well-supported in +opam-repository, thanks to the previous efforts in opam-repository-mingw. +The MSVC port is Visual Studio-based. At +present, there is less support in this ecosystem for external dependencies, +though this is something we expect to work on both in opam-repository and in +subsequent opam releases. In particular, it is necessary to install +Visual Studio or Visual Studio BuildTools separately, but opam will then +automatically find and use the C compiler from Visual Studio.

+

Major change: opam tree / opam why

+

opam tree is a new command showing packages and their dependencies with a tree view. +It is very helpful to determine which packages bring which dependencies in your installed switch.

+
$ opam tree cppo
+cppo.1.6.9
+├── base-unix.base
+├── dune.3.8.2 (>= 1.10)
+│   ├── base-threads.base
+│   ├── base-unix.base [*]
+│   └── ocaml.4.14.1 (>= 4.08)
+│       ├── ocaml-base-compiler.4.14.1 (>= 4.14.1~ & < 4.14.2~)
+│       └── ocaml-config.2 (>= 2)
+│           └── ocaml-base-compiler.4.14.1 (>= 4.12.0~) [*]
+└── ocaml.4.14.1 (>= 4.02.3) [*]
+
+

Reverse-dependencies can also be displayed using the new opam why command. +This is useful to examine how dependency versions get constrained.

+
$ opam why cmdliner
+cmdliner.1.2.0
+├── (>= 1.1.0) b0.0.0.5
+│   └── (= 0.0.5) odig.0.0.9
+├── (>= 1.1.0) ocp-browser.1.3.4
+├── (>= 1.0.0) ocp-indent.1.8.1
+│   └── (>= 1.4.2) ocp-index.1.3.4
+│       └── (= version) ocp-browser.1.3.4 [*]
+├── (>= 1.1.0) ocp-index.1.3.4 [*]
+├── (>= 1.1.0) odig.0.0.9 [*]
+├── (>= 1.0.0) odoc.2.2.0
+│   └── (>= 2.0.0) odig.0.0.9 [*]
+├── (>= 1.1.0) opam-client.2.2.0~alpha
+│   ├── (= version) opam.2.2.0~alpha
+│   └── (= version) opam-devel.2.2.0~alpha
+├── (>= 1.1.0) opam-devel.2.2.0~alpha [*]
+├── (>= 0.9.8) opam-installer.2.2.0~alpha
+└── user-setup.0.7
+
+
+

Special thanks to @cannorin for contributing this feature.

+
+

Major change: with-dev-setup

+

There is now a way for a project maintainer to share their project development +tools: the with-dev-setup dependency flag. It is used in the same way as +with-doc and with-test: by adding a {with-dev-setup} filter after a +dependency. It will be ignored when installing normally, but it's pulled in when the +package is explicitly installed with the --with-dev-setup flag specified on +the command line.

+

For example

+
opam-version: "2.0"
+depends: [
+  "ocaml"
+  "ocp-indent" {with-dev-setup}
+]
+build: [make]
+install: [make "install"]
+post-messages:
+[ "Thanks for installing the package"
+  "as well as its development setup. It will help with your future contributions" {with-dev-setup} ]
+
+

Major change: opam pin --recursive

+

When pinning a package using opam pin, opam looks for opam files in the root directory only. +With recursive pinning, you can now instruct opam to look for .opam files in +subdirectories as well, while maintaining the correct relationship between the .opam +files and the package root for versioning and build purposes.

+

Recursive pinning is enabled by the following options to opam pin and opam install:

+ +

The two options can be combined: for instance, if your opam packages are stored +as a deep hierarchy in the mylib subdirectory of your project you can try +opam pin . --recursive --subpath mylib.

+

These options are useful when dealing with a large monorepo-type repository with many +opam libraries spread about.

+

New Options

+ +

Miscellaneous changes

+ +

And many other general and performance improvements were made and bugs were fixed. +You can take a look to previous blog posts. +API changes and a more detailed description of the changes are listed in:

+ +

This release also includes PRs improving the documentation and improving +and extending the tests.

+

Please report any issues to the bug-tracker.

+

We hope you will enjoy the new features of opam 2.2! 📯

+ diff --git a/data/planet/ocamlpro/optimisation-de-geneweb-1er-logiciel-franais-de-gnalogie-depuis-prs-de-30-ans.md b/data/planet/ocamlpro/optimisation-de-geneweb-1er-logiciel-franais-de-gnalogie-depuis-prs-de-30-ans.md new file mode 100644 index 0000000000..a8bc23c6ee --- /dev/null +++ b/data/planet/ocamlpro/optimisation-de-geneweb-1er-logiciel-franais-de-gnalogie-depuis-prs-de-30-ans.md @@ -0,0 +1,54 @@ +--- +title: "Optimisation de Geneweb, 1er logiciel fran\xE7ais de G\xE9n\xE9alogie depuis + pr\xE8s de 30 ans" +description: "L\u2019\xE9quipe d\u2019OCamlPro a r\xE9cemment \xE9t\xE9 sollicit\xE9e + par l\u2019association Roglo, une association fran\xE7aise de g\xE9n\xE9alogie qui + g\xE8re une base de plus de 10 millions de personnes connect\xE9es dans un m\xEAme + arbre g\xE9n\xE9alogique, et dont la base s'accro\xEEt d\u2019environ 500 000 nouvelles + contributions ..." +url: https://ocamlpro.com/blog/2024_11_06_short_news_archeologie_de_la_genealogie +date: 2024-11-06T16:50:25-00:00 +preview_image: https://ocamlpro.com/blog/assets/img/og_genealogy_tree.png +authors: +- "\n Fabrice Le Fessant\n " +source: +--- + +

+

+

+

+ + Un bonsaï sous sa cloche de verre. De nos jours, l'accès à la généalogie grand public est préservé surtout grâce à la maintenance de codes patrimoniaux. + +

+ Un bonsaï sous sa cloche de verre. De nos jours, l'accès à la généalogie grand public est préservé surtout grâce à la maintenance de codes patrimoniaux. +
+ +
+ +

L’équipe d’OCamlPro a récemment été sollicitée par l’association Roglo, une +association française de généalogie qui gère une base de plus de 10 millions de +personnes connectées dans un même arbre généalogique, et dont la base +s'accroît d’environ 500 000 nouvelles contributions tous les ans. L’association +s’appuie sur le logiciel libre Geneweb, l’un des plus puissants logiciels +du domaine, créé en 1997 à l’Inria, permettant de partager sur le web des +arbres généalogiques, et utilisé aussi bien par des particuliers que par des +leaders du secteur, comme la société française Geneanet, acquise en 2021 par +l’Américain Ancestry.

+

Notre mission s’est d’abord concentrée sur l'optimisation des performances, +pour ramener le traitement de certaines requêtes sur la base gargantuesque de +Roglo à des temps raisonnables. Après avoir rapidement survolé le code de plus +de 80 000 lignes et profilé les requêtes les plus coûteuses, nous avons pu +proposer une solution, l’implanter et l’intégrer dans la branche principale. +Pour l’une des requêtes, le temps passe ainsi de 77s à 4s, soit 18 fois plus +rapide ! Nous travaillons maintenant à enrichir Geneweb de nouvelles +fonctionnalités pour ces utilisateurs, mais aussi pour ses contributeurs et les +mainteneurs de la plateforme !

+

Cette mission, fragmentée en sprints de développement, s'inscrit dans une +démarche continue visant à faire évoluer Geneweb pour qu'il puisse gérer des +volumes de données encore plus importants. +Nous sommes ravis de contribuer à cette évolution, en apportant notre expertise +en optimisation et en développement logiciel pour faire grandir cette +plateforme de référence.

+ diff --git a/data/planet/signalsandthreads/from-the-lab-to-the-trading-floor-with-erin-murphy.md b/data/planet/signalsandthreads/from-the-lab-to-the-trading-floor-with-erin-murphy.md new file mode 100644 index 0000000000..d86765879d --- /dev/null +++ b/data/planet/signalsandthreads/from-the-lab-to-the-trading-floor-with-erin-murphy.md @@ -0,0 +1,13 @@ +--- +title: From the Lab to the Trading Floor with Erin Murphy +description: +url: https://signals-threads.simplecast.com/episodes/from-the-lab-to-the-trading-floor-with-erin-murphy-hD6GHMhc +date: 2024-07-12T19:15:09-00:00 +preview_image: +authors: +- Signals and Threads +source: +--- + +

Erin Murphy is Jane Street’s first UX designer, and before that, she worked at NASA’s Jet Propulsion Laboratory building user interfaces for space missions. She’s also an illustrator with her own quarterly journal. In this episode, Erin and Ron discuss the challenge of doing user-centered design in an organization where experts are used to building tools for themselves. How do you bring a command-line interface to the web without making it worse for power users? They also discuss how beauty in design is more about utility than aesthetics; what Jane Street looks for in UX candidates; and how to help engineers discover what their users really want.

You can find the transcript for this episode  on our website.

Some links to topics that came up in the discussion:

+ diff --git a/data/planet/signalsandthreads/solving-puzzles-in-production-with-liora-friedberg.md b/data/planet/signalsandthreads/solving-puzzles-in-production-with-liora-friedberg.md new file mode 100644 index 0000000000..1a38227b5f --- /dev/null +++ b/data/planet/signalsandthreads/solving-puzzles-in-production-with-liora-friedberg.md @@ -0,0 +1,13 @@ +--- +title: Solving Puzzles in Production with Liora Friedberg +description: +url: https://signals-threads.simplecast.com/episodes/solving-puzzles-in-production-with-liora-friedberg-dk6vYnK2 +date: 2024-10-07T15:50:40-00:00 +preview_image: +authors: +- Signals and Threads +source: +--- + +

Liora Friedberg is a Production Engineer at Jane Street with a background in economics and computer science. In this episode, Liora and Ron discuss how production engineering blends high-stakes puzzle solving with thoughtful software engineering, as the people doing support build tools to make that support less necessary. They also discuss how Jane Street uses both tabletop simulation and hands-on exercises to train Production Engineers; what skills effective Production Engineers have in common; and how to create a culture where people aren’t blamed for making costly mistakes.

You can find the transcript for this episode  on our website.

Some links to topics that came up in the discussion:

+ diff --git a/data/planet/signalsandthreads/the-uncertain-art-of-accelerating-ml-models-with-sylvain-gugger.md b/data/planet/signalsandthreads/the-uncertain-art-of-accelerating-ml-models-with-sylvain-gugger.md new file mode 100644 index 0000000000..8b4ce959eb --- /dev/null +++ b/data/planet/signalsandthreads/the-uncertain-art-of-accelerating-ml-models-with-sylvain-gugger.md @@ -0,0 +1,13 @@ +--- +title: The Uncertain Art of Accelerating ML Models with Sylvain Gugger +description: +url: https://signals-threads.simplecast.com/episodes/the-uncertain-art-of-accelerating-ml-models-with-sylvain-gugger-moYuL4Ps +date: 2024-10-14T14:47:42-00:00 +preview_image: +authors: +- Signals and Threads +source: +--- + +

Sylvain Gugger is a former math teacher who fell into machine learning via a MOOC and became an expert in the low-level performance details of neural networks. He’s now on the ML infrastructure team at Jane Street, where he helps traders speed up their models. In this episode, Sylvain and Ron go deep on learning rate schedules; the subtle performance bugs PyTorch lets you write; how to keep a hungry GPU well-fed; and lots more, including the foremost importance of reproducibility in training runs. They also discuss some of the unique challenges of doing ML in the world of trading, like the unusual size and shape of market data and the need to do inference at shockingly low latencies.

You can find the transcript for this episode  on our website.

Some links to topics that came up in the discussion:

+ diff --git a/data/planet/talex5/ocaml-5-performance-part-2.md b/data/planet/talex5/ocaml-5-performance-part-2.md new file mode 100644 index 0000000000..b54594ef6e --- /dev/null +++ b/data/planet/talex5/ocaml-5-performance-part-2.md @@ -0,0 +1,959 @@ +--- +title: OCaml 5 performance part 2 +description: +url: https://roscidus.com/blog/blog/2024/07/22/performance-2/ +date: 2024-07-22T11:00:00-00:00 +preview_image: +authors: +- Thomas Leonard +source: +--- + +

The last post looked at using various tools to understand why an OCaml 5 program was waiting a long time for IO. +In this post, I'll be trying out some tools to investigate a compute-intensive program that uses multiple CPUs.

+ +

Table of Contents

+ +

Further discussion about this post can be found on discuss.ocaml.org.

+

The problem

+

OCaml 4 allowed running multiple "system threads", but only one can have the OCaml runtime lock, +so only one can be running OCaml code at a time. +OCaml 5 allows running multiple "domains", all of which can be running OCaml code at the same time +(each domain can also have multiple system threads; only one system thread can be running OCaml code per domain).

+

The ocaml-ci service provides CI for many OCaml programs, +and its first step when testing a commit is to run a solver to select compatible versions for its dependencies. +Running a solve typically only takes about a second, but it has to do it for each possible test platform, +which includes versions of the OCaml compiler from 4.02 to 4.14 and 5.0 to 5.2, +multiple architectures (32-bit and 64-bit x86, 32-bit and 64-bit ARM, PPC64 and s390x), +operating systems (Alpine, Debian, Fedora, FreeBSD, macos, OpenSUSE and Ubuntu, in multiple versions), etc. +In total, this currently does 132 solver runs per commit being tested +(which seems too high to me, but let's ignore that for now).

+

The solves are done by the solver-service, +which runs on a couple of ARM machines with 160 cores each. +The old OCaml 4 version used to work by spawning lots of sub-processes, +but when OCaml 5 came out, I ported it to use a single process with multiple domains. +That removed the need for lots of communication logic, +and allowed sharing common data such as the package definitions. +The code got a lot shorter and simpler, and I'm told it's been much more reliable too.

+

But the performance was surprisingly bad. +Here's a graph showing how the number of solves per second scales with the number of CPUs (workers) being used:

+

Processes scaling better than domains

+

The "Processes" line shows performance when forking multiple processes to do the work, which looks pretty good. +The "Domains" line shows what happens if you instead spawn domains inside a single process.

+

Note: The original service used many libraries (a mix of Eio and Lwt ones), +but to make investigation easier I simplified it by removing most of them. +The simplified version doesn't use Eio or Lwt; +it just spawns some domains/processes and has each of them do the same solve in a loop a fixed number of times.

+

ThreadSanitizer

+

When converting a single-domain OCaml 4 program to use multiple cores it's easy to introduce races. +OCaml has ThreadSanitizer (TSan) support which can detect these. +To use it, install an OCaml compiler with the tsan option:

+
$ opam switch create 5.2.0-tsan ocaml-variants.5.2.0+options ocaml-option-tsan
+
+

Things run a lot slower and require more memory with this compiler, but it's good to check:

+
$ ./_build/default/stress/stress.exe --internal-workers=2
+[...]
+WARNING: ThreadSanitizer: data race (pid=133127)
+  Write of size 8 at 0x7ff2b7814d38 by thread T4 (mutexes: write M88):
+    #0 camlOpam_0install__Model.group_ors_1288 lib/model.ml:70 (stress.exe+0x1d2bba)
+    #1 camlOpam_0install__Model.group_ors_1288 lib/model.ml:120 (stress.exe+0x1d2b47)
+    ...
+
+  Previous write of size 8 at 0x7ff2b7814d38 by thread T1 (mutexes: write M83):
+    #0 camlOpam_0install__Model.group_ors_1288 lib/model.ml:70 (stress.exe+0x1d2bba)
+    #1 camlOpam_0install__Model.group_ors_1288 lib/model.ml:120 (stress.exe+0x1d2b47)
+    ...
+
+  Mutex M88 (0x558368b95358) created at:
+    #0 pthread_mutex_init ../../../../src/libsanitizer/tsan/tsan_interceptors_posix.cpp:1295 (libtsan.so.2+0x50468)
+    #1 caml_plat_mutex_init runtime/platform.c:57 (stress.exe+0x4763b2)
+    #2 caml_init_domains runtime/domain.c:943 (stress.exe+0x44ebfe)
+    ...
+
+  Mutex M83 (0x558368b95240) created at:
+    #0 pthread_mutex_init ../../../../src/libsanitizer/tsan/tsan_interceptors_posix.cpp:1295 (libtsan.so.2+0x50468)
+    #1 caml_plat_mutex_init runtime/platform.c:57 (stress.exe+0x4763b2)
+    #2 caml_init_domains runtime/domain.c:943 (stress.exe+0x44ebfe)
+    ...
+
+  Thread T4 (tid=133132, running) created by main thread at:
+    #0 pthread_create ../../../../src/libsanitizer/tsan/tsan_interceptors_posix.cpp:1001 (libtsan.so.2+0x5e686)
+    #1 caml_domain_spawn runtime/domain.c:1265 (stress.exe+0x4504c4)
+    ...
+
+  Thread T1 (tid=133129, running) created by main thread at:
+    #0 pthread_create ../../../../src/libsanitizer/tsan/tsan_interceptors_posix.cpp:1001 (libtsan.so.2+0x5e686)
+    #1 caml_domain_spawn runtime/domain.c:1265 (stress.exe+0x4504c4)
+    ...
+
+SUMMARY: ThreadSanitizer: data race lib/model.ml:70 in camlOpam_0install__Model.group_ors_1288
+
+

The two mutexes mentioned in the output, M83 and M88, are the domain_lock, +used to ensure only one sys-thread runs at a time in each domain. +In this program we only have one sys-thread per domain and so can ignore them.

+

The output reveals that the solver used a global variable to generate unique IDs:

+
1
+2
+3
+4
+5
+
let fresh_id =
+  let i = ref 0 in
+  fun () ->
+    incr i;           (* model.ml:70 *)
+    !i
+

With that fixed, TSan finds no further problems (in this simplified version). +This gives us good confidence that there isn't any shared state: +TSan would report use of shared state not protected by a mutex, +and since the program was written for OCaml 4 it won't be using any mutexes.

+

That's good, because if one thread writes to a location that another reads then that requires coordination between CPUs, +which is relatively slow +(though we could still experience slow-downs due to false sharing, +where two separate mutable items end up in the same cache line). +However, while important for correctness, it didn't make any noticeable difference to the benchmark results.

+

perf

+

perf is the obvious tool to use when facing CPU performance problems. +perf record -g PROG takes samples of the program's stack regularly, +so that functions that run a lot or for a long time will appear often. +perf report provides a UI to explore the results:

+
$ perf report
+  Children      Self  Command     Shared Object      Symbol
++   59.81%     0.00%  stress.exe  stress.exe         [.] Zeroinstall_solver.Solver_core.do_solve_2283
++   59.44%     0.00%  stress.exe  stress.exe         [.] Opam_0install.Solver.solve_1428
++   59.25%     0.00%  stress.exe  stress.exe         [.] Dune.exe.Domain_worker.solve_951
++   58.88%     0.00%  stress.exe  stress.exe         [.] Dune.exe.Stress.run_worker_332
++   58.18%     0.00%  stress.exe  stress.exe         [.] Stdlib.Domain.body_735
++   57.91%     0.00%  stress.exe  stress.exe         [.] caml_start_program
++   34.39%     0.69%  stress.exe  stress.exe         [.] Stdlib.List.iter_366
++   34.39%     0.03%  stress.exe  stress.exe         [.] Zeroinstall_solver.Solver_core.lookup_845
++   34.39%     0.09%  stress.exe  stress.exe         [.] Zeroinstall_solver.Solver_core.process_dep_2024
++   33.14%     0.03%  stress.exe  stress.exe         [.] Zeroinstall_solver.Sat.run_solver_1446
++   27.28%     0.00%  stress.exe  stress.exe         [.] Zeroinstall_solver.Solver_core.build_problem_2092
++   26.27%     0.02%  stress.exe  stress.exe         [.] caml_call_gc
+
+

Looks like we're spending most of our time solving, as expected. +But this can be misleading. +Because perf only records stack traces when the code is running, it doesn't report any time the process spent sleeping.

+
$ /usr/bin/time ./_build/default/stress/stress.exe --count=10 --internal-workers=7
+73.08user 0.61system 0:12.65elapsed 582%CPU (0avgtext+0avgdata 596608maxresident)k
+
+

With 7 workers, we'd expect to see 700%CPU, but we only see 582%.

+

mpstat

+

mpstat can show a per-CPU breakdown. +Here are a couple of one second intervals on my machine while the solver was running:

+
$ mpstat --dec=0 -P ALL 1
+16:24:39     CPU    %usr   %sys %iowait    %irq   %soft  %steal   %idle
+16:24:40     all      78      1       2       1       0       0      18
+16:24:40       0      19      1       0       1       0       1      78
+16:24:40       1      88      1       0       1       0       0      10
+16:24:40       2      88      1       0       1       0       0      10
+16:24:40       3      88      0       0       0       0       1      11
+16:24:40       4      89      1       0       0       0       0      10
+16:24:40       5      90      0       0       1       0       0       9
+16:24:40       6      79      1       0       1       1       1      17
+16:24:40       7      86      0      12       1       1       0       0
+
+16:24:40     CPU    %usr   %sys %iowait    %irq   %soft  %steal   %idle
+16:24:41     all      80      1       2       1       0       0      17
+16:24:41       0      85      0      12       1       0       1       1
+16:24:41       1      91      1       0       1       0       0       7
+16:24:41       2      90      0       0       1       1       0       8
+16:24:41       3      89      1       0       1       0       0       9
+16:24:41       4      67      1       0       1       0       0      31
+16:24:41       5      52      1       0       0       0       1      46
+16:24:41       6      76      1       0       1       0       0      22
+16:24:41       7      90      1       0       0       0       0       9
+
+

Note: I removed some columns with all zero values to save space.

+

We might expect to see 7 CPUs running at 100% and one idle CPU, +but in fact they're all moderately busy. +On the other hand, none of them spent more than 91% of its time running the solver code.

+

offcputime

+

offcputime will show why a process wasn't using a CPU +(it's like offwaketime, which we saw earlier, but doesn't record the waker). +Here I'm using pidstat to see all running threads and then examining one of the workers, +to avoid the problem we saw last time where the diagram included multiple threads:

+
$ pidstat 1 -t
+...
+^C
+Average:      UID      TGID       TID    %usr %system  %guest   %wait    %CPU   CPU  Command
+Average:     1000     78304         -  550.50    9.41    0.00    0.00  559.90     -  stress.exe
+Average:     1000         -     78305   91.09    1.49    0.00    0.00   92.57     -  |__stress.exe
+Average:     1000         -     78307    8.42    0.99    0.00    0.00    9.41     -  |__stress.exe
+Average:     1000         -     78308   90.59    1.49    0.00    0.00   92.08     -  |__stress.exe
+Average:     1000         -     78310   90.59    1.49    0.00    0.00   92.08     -  |__stress.exe
+Average:     1000         -     78312   91.09    1.49    0.00    0.00   92.57     -  |__stress.exe
+Average:     1000         -     78314   89.11    1.49    0.00    0.00   90.59     -  |__stress.exe
+Average:     1000         -     78316   89.60    1.98    0.00    0.00   91.58     -  |__stress.exe
+
+$ sudo offcputime-bpfcc -f -t 78310 > off-cpu
+
+

Note: The ARM machine's kernel was too old to run offcputime, so I ran this on my machine instead, +with one main domain and six workers. +As I needed good stacks for C functions too, I ran stress.exe in an Ubuntu 24.04 docker container, +as recent versions of Ubuntu compile with frame pointers by default.

+

The raw output was very noisy, showing it waiting in many different places. +Looking at a few, it was clear it was mostly the GC (which can run from almost anywhere). +The output is just a text-file with one line per stack-trace, and bit of sed cleaned it up:

+
$ sed -E 's/stress.exe;.*;(caml_call_gc|caml_handle_gc_interrupt|caml_poll_gc_work|asm_sysvec_apic_timer_interrupt|asm_sysvec_reschedule_ipi);/stress.exe;\\1;/' off-cpu > off-cpu-gc
+$ flamegraph.pl --colors=blue off-cpu-gc > off-cpu-gc.svg
+
+

That removes the part of the stack-trace before any of various interrupt-type functions that can be called from anywhere. +The graph is blue to indicate that it shows time when the process wasn't running.

+

Time spent off-CPU

+

There are rather a lot of traces where we missed the user stack. +However, the results seem clear enough: when our worker is waiting, it's in the garbage collector, +calling caml_plat_spin_wait. +This is used to sleep when a spin-lock has been spinning for too long (after 1000 iterations).

+

The OCaml garbage collector

+

OCaml has a major heap for long-lived values, plus one fixed-size minor heap for each domain. +New allocations are made sequentially on the allocating domain's minor heap +(which is very fast, just adjusting a pointer by the size required).

+

When the minor heap is full the program performs a minor GC, +moving any values that are still reachable to the major heap +and leaving the minor heap empty.

+

Garbage collection of the major heap is done in small slices so that the application doesn't pause for long, +and domains can do marking and sweeping work without needing to coordinate +(except at the very end of a major cycle, when they briefly synchronise to agree a new cycle is starting).

+

However, as minor GCs move values that other domains may be using, they do require all domains to stop.

+

Although the simplified test program doesn't use Eio, we can still use eio-trace to record GC events +(we just don't see any fibers). +Here's a screenshot of the solver running with 24 domains on the ARM machine, +showing it performing GC work (not all domains are visible in the picture):

+

GC work shown in eio-trace

+ +

The orange/red parts show when the GC is running and the yellow regions show when the domain is waiting for other domains. +The thick columns with yellow edges are minor GCs, +while the thin (almost invisible) red columns without any yellow between them are major slices. +The second minor GC from the left took longer than usual because the third domain from the top took a while to respond. +It also didn't do a major slice before that; perhaps it was busy doing something, or maybe Linux scheduled a different process to run then.

+

Traces recorded by eio-trace can also be viewed in Perfetto, which shows the nesting better: +Here's a close-up of a single minor GC, corresponding to the bottom two domains from the second column from the left:

+

Close-up in Perfetto

+ +

We can now see why the solver spends so much time sleeping; +when a domain performs a minor GC, it spends most of the time waiting for other domains.

+

(the above is a slight simplification; domains may do some work on the major GC while waiting)

+

statmemprof

+

One obvious solution to GC slowness is to produce less garbage in the first place. +To do that, we need to find out where the most costly allocations are coming from. +Tracing every memory allocation tends to make programs unusably slow, +so OCaml instead provides a statistical memory profiler.

+

It was temporarily removed in OCaml 5 because it needed updating for the new multicore GC, +but has recently been brought back and will be in OCaml 5.3. +There's a backport to 5.2, but I couldn't get it to work, +so I just removed the domains stuff from the test and did a single-domain run on OCaml 4.14. +You need the memtrace library to collect samples and memtrace_viewer to view them:

+
$ opam install memtrace memtrace_viewer
+
+

Put this at the start of the program to enable it:

+
1
+
let () = Memtrace.trace_if_requested ~context:"solver-test" ()
+

Then running with MEMTRACE set records a trace:

+
$ MEMTRACE=solver.ctf ./stress.exe --count=10
+Solved warm-up request in: 1.99s
+Running another 10 * 1 solves...
+
+$ memtrace-viewer solver.ctf
+Processing solver.ctf...
+Serving http://localhost:8080/
+
+

The memtrace viewer UI

+

The flame graph in the middle shows functions scaled by the amount of memory they allocated. +Initially it showed two groups, one for the warm-up request and one for the 10 runs. +To simplify the display, I used the filter panel (on the left) to show only allocations after the 2 second warm-up. +We can immediately see that OpamVersionCompare.compare is the source of most memory use.

+

Focusing on that function shows that it performed 54.1% of all allocations. +The display now shows allocations performed within it above it (in green), +and all the places it's called from in blue below:

+

The compare function is expensive!

+

The bulk of the allocations are coming from this loop:

+
1
+2
+3
+4
+5
+6
+7
+8
+9
+10
+
(* [skip_while_from i f w m] yields the index of the leftmost character
+ * in the string [s], starting from [i], and ending at [m], that does
+ * not satisfy the predicate [f], or [length w] if no such index exists.  *)
+let skip_while_from i f w m =
+  let rec loop i =
+    if i = m then i
+    else if f w.[i] then loop (i + 1) else i
+  in loop i
+
+let skip_zeros x xi xl = skip_while_from xi (fun c -> c = '0') x xl
+

It's used when processing a version like 1.2.3 to skip any leading "0" characters +(so that would compare equal to 1.02.3). +The loop function refers to other variables (such as f) from its context, +and so OCaml allocates a closure on the heap to hold these variables. +Even though these allocations are small, we have to do it for every component of every version. +And we compare versions a lot: +for every version of a package that says it requires e.g. libfoo { >= "1.2" }, +we have to check the formula against every version of libfoo.

+

The solution is rather simple (and shorter than the original!):

+
1
+2
+3
+
let rec skip_while_from i f w m =
+  if i = m then i
+  else if f w.[i] then skip_while_from (i + 1) f w m else i
+

Removing the other allocations from compare too reduces total memory allocations +from 21.8G to 9.6G! +The processes benchmark got about 14% faster, while the domains one was 23% faster:

+

Effect of reducing allocations. Old values are shown in grey.

+

A nice optimisation, +but using domains is still nowhere close to even the original version with separate processes.

+

magic-trace

+

The traces above show the solver taking a long time for all domains to enter the stw_api_barrier phase. +What was the slow domain doing to cause that? +magic-trace lets us tell it when to save the ring buffer and we can use this to get detailed information. +Tracing multiple threads with magic-trace doesn't seem to work well +(each thread gets a very small buffer, they don't stop at quite the same time, and triggers don't work) +so I find it's better to trace just one thread.

+

I modified the OCaml runtime so that the leader (the domain requesting the GC) records the time. +As each domain enters stw_api_barrier it checks how late it is and calls a function to print a warning if it's above a threshold. +Then I attached magic-trace to one of the worker threads and told it to save a sample when that function got called:

+

A domain being slow to join a minor GC

+

In the example above, +magic-trace saved about 7ms of the history of a domain up to the point where it entered stw_api_barrier. +The first few ms show the solver working normally. +Then it needs to do a minor GC and tries to become the leader. +But another domain has the lock and so it spins, calling handle_incoming 293,711 times in a loop for 2.5ms.

+

I had a look at the code in the OCaml runtime. +When a domain wants to perform a minor GC, the steps are:

+
    +
  1. Acquire all_domains_lock. +
    2. +
  2. Populate the stw_request global. +
    3. +
  3. Interrupt all domains. +
    4. +
  4. Release all_domains_lock. +
    5. +
  5. Wait for all domains to get the interrupt. +
    6. +
  6. Mark self as ready, allowing GC work to start. +
    7. +
  7. Do minor GC. +
    8. +
  8. The last domain to finish its minor GC signals all_domains_cond and everyone resumes. +
    9. +
+

I added some extra event reporting to the GC, showing when a domain is trying to perform a GC (try), +when the leader is signalling other domains (signal), and when a domain is sleeping waiting for something (sleep). +Here's what that looks like (in some places):

+

One sleeping domain delays all the others

+
    +
  1. The top domain finished its minor collection quickly (as it's mostly idle and had nothing to do), +and started waiting for the other domains to finish. For some reason, this sleep call took 3ms to run. +
    2. +
  2. The other domains resume work. One by one, they fill their minor heaps and try to start a GC. +
    3. +
  3. They can't start a new GC, as the old one hasn't completely finished yet, so they spin. +
    4. +
  4. Eventually the top domain wakes up and finishes the previous STW section. +
    5. +
  5. One of the other domains immediately starts a new minor GC and the pattern repeats. +
    6. +
+

These try events seem useful; +the program is spending much more time stuck in GC than the original traces indicated!

+

One obvious improvement here would be for idle domains to opt out of GC. +Another would be to tell the kernel when to wake instead of using sleeps — +and I see there's a PR already: +OS-based Synchronisation for Stop-the-World Sections.

+

Another possibility would be to let domains perform minor GCs independently. +The OCaml developers did make a version that worked that way, +but it requires changes to all C code that uses the OCaml APIs, +since a value in another domain's minor heap might move while it's running.

+

Finally, I wonder if the code could be simplified a bit using a compare-and-set instead of taking a lock to become leader. +That would eliminate the try state, where a domain knows another domain is the leader, but doesn't know what it wants to do. +It's also strange that there's a state where +the top domain has finished its critical section and allowed the other domains to resume, +but is not quite finished enough to let a new GC start.

+

We can work around this problem by having the main domain do work too. +That could be a problem for interactive applications (where the main domain is running the UI and needs to respond fast), +but it should be OK for the solver service. +This was about 15% faster on my machine, but appeared to have no effect on the ARM server. +Lesson: get traces on the target machine!

+

Tuning GC parameters

+

Another way to reduce the synchronisation overhead of minor GCs is to make them less frequent. +We can do that by increasing the size of the minor heap, +doing a few long GCs rather than many short ones. +The size is controlled by the setting e.g. OCAMLRUNPARAM=s=8192k. +On my machine, this actually makes things slower, but it's about 18% faster on the ARM server with 80 domains.

+

Here are the first few domains (from a total of 24) on the ARM server with different minor heap sizes +(both are showing 1s of execution):

+

The default minor heap size (256k words) +With a larger minor heap (8192k works) +Note that the major slices also get fewer and larger, as they happen half way between minor slices.

+

Also, there's still a lot of variation between the time each domain spends doing GC +(despite the fact that they're all running exactly the same task), so they still end up waiting a lot.

+

Simplifying further

+

This is all still pretty odd, though. +We're getting small performance increases, but still nothing like when forking. +Can the test-case be simplified further? +Yes, it turns out! +This simple function takes much longer to run when using domains, compared to forking!

+
1
+2
+3
+4
+
let run_worker n =
+  for _i = 1 to n * 10000000 do
+    ignore (Sys.opaque_identity (ref ()))
+  done
+

ref () allocates a small block (2 words, including the header) on the minor heap. +opaque_identity is to make sure the compiler doesn't optimise this pointless allocation away.

+

Time to run the loop on the 160-core ARM server (lower is better)

+

Here's what I would expect here:

+
    +
  1. The domains all start to fill their minor heaps. One fills it and triggers a minor GC. +
    2. +
  2. The triggering domain sets an indicator in each domain saying a GC is due. +None of the domains is sleeping, so the OS isn't involved in any wake-ups here. +
    3. +
  3. The other domains check the indicator on their next allocation, +which happens immediately since that's all they're doing. +
    4. +
  4. The GCs all proceed quickly, since there's nothing to scan and nothing to promote +(except possibly the current single allocation). +
    5. +
  5. They all resume quickly and continue. +
    6. +
+

So ideally the lines would be flat. +In practice, we may hit physical limits due to memory bandwidth, CPU temperature or kernel limitations; +I assume this is why the "Processes" time starts to rise eventually. +But it looks like this minor slow-down causes knock-on effects in the "Domains" case.

+

If I remove the allocation, then the domains and processes versions take the same amount of time.

+

perf sched

+

perf sched record records kernel scheduling events, allowing it to show what is running on each CPU at all times. +perf sched timehist displays a report:

+
$ sudo perf sched record -k CLOCK_MONOTONIC
+^C
+
+$ sudo perf sched timehist
+           time    cpu  task name                       wait time  sch delay   run time
+                        [tid/pid]                          (msec)     (msec)     (msec)
+--------------- ------  ------------------------------  ---------  ---------  ---------
+  185296.715345 [0000]  sway[175042]                        1.694      0.025      0.775 
+  185296.716024 [0002]  crosvm_vcpu2[178276/178217]         0.012      0.000      2.957 
+  185296.717031 [0003]  main.exe[196519]                    0.006      0.000      4.004 
+  185296.717044 [0003]  rcu_preempt[18]                     4.004      0.015      0.012 
+  185296.717260 [0001]  main.exe[196526]                    1.760      0.000      2.633 
+  185296.717455 [0001]  crosvm_vcpu1[193502/193445]        63.809      0.015      0.194 
+  ...
+
+

The first line here shows that sway needed to wait for 1.694 ms for some reason (possibly a sleep), +and then once it was due to resume, had to wait a further 0.025 ms for CPU 0 to be free. It then ran for 0.775 ms. +I decided to use perf sched to find out what the system was doing when a domain failed to respond quickly.

+

To make the output easier to read, I hacked eio-trace to display it on the traces. +perf script -g python will generate a skeleton Python script that can format all the events found in the perf.data file, +and I used that to convert the output to CSV. +To correlate OCaml domains with Linux threads, I also modified OCaml to report the thread ID (TID) for each new domain +(it was previously reporting the PID instead for some reason).

+

Here's a trace of the simple allocator from the previous section:

+

eio-trace with perf sched data

+ +

Note: the colour of stw_api_barrier has changed: previously eio-trace coloured it yellow to indicate sleeping, +but now we have the individual sleep events we can see exactly which part of it was sleeping.

+

The horizontal green bars show when each domain was running on the CPU. +Here, we see that most of the domains ran until they called sleep. +When the sleep timeout expires, the thread is ready to run again and goes on the run-queue. +Time spent waiting on the queue is shown with a black bar.

+

When switching to or from another process, the process name is shown. +Here we can see that crosvm_vcpu6 interrupted one of our domains, making it late to respond to the GC request.

+

Here we see another odd feature of the protocol: even though the late domain was the last to be ready, +it wasn't able to start its GC even then, because only the leader is allowed to say when everyone is ready. +Several domains wake after the late one is ready and have to go back to sleep again.

+

The diagram also shows when Linux migrated our OCaml domains between CPUs. +For example:

+
    +
  1. The bottom domain was initially running on CPU 0. +
    2. +
  2. After sleeping briefly, it spent a while waiting to resume and Linux moved it to CPU 6 (the leader domain, which was idle then). +
    3. +
  3. Once there, the bottom domain slept briefly again, and again was slow to wake, getting moved to CPU 7. +
    4. +
+

Here's another example:

+

Two domains on the same CPU

+
    +
  1. The bottom domain's sleep finished a while ago, and it's been stuck on the queue because it's on the same CPU as another domain. +
    2. +
  2. All the other domains are spinning, trying to become the leader for the next minor GC. +
    3. +
  3. Eventually, Linux preempts the 5th domain from the top to run the bottom domain +(the vertical green line indicates a switch between domains in the same process). +
    4. +
  4. The bottom domain finishes the previous minor GC, allowing the 3rd from top to start a new one. +
    5. +
  5. The new GC is delayed because the 5th domain is now waiting while the bottom domain spins. +
    6. +
  6. Eventually the bottom domain sleeps, allowing 5 to join and the GC starts. +
    7. +
+

I tried using the processor package to pin each domain to a different CPU. +That cleaned up the traces a fair bit, but didn't make much difference to the runtime on my machine.

+

I also tried using chrt to run the program as a high-priority "real-time" task, +which also didn't seem to help. +I wrote a bpftrace script to report if one of our domains was ready to resume and the scheduler instead ran something else. +That showed various things. +Often Linux was migrating something else out of the way and we had to wait for that, +but there were also some kernel tasks that seemed to be even higher priority, such as GPU drivers or uring workers. +I suspect to make this work you'd need to set the affinity of all the other processes to keep them away from the cores being used +(but that wouldn't work in this example because I'm using all of them!). +Come to think of it, running a CPU intensive task on every CPU at realtime priority was a dumb idea; +had it worked I wouldn't have been able to do anything else with the computer!

+

olly

+

Exploring the scheduler behaviour was interesting, and might be needed for latency-sensitive tasks, +but how often do migrations and delays really cause trouble? +The slow GCs are interesting, but there are also sections like this where everything is going smoothly, +and minor GCs take less than 4 microseconds:

+

GCs going well

+

olly can be used get summary statistics:

+
$ olly gc-stats './_build/default/stress/stress.exe --count=6 --internal-workers=24'
+...
+Solved 144 requests in 25.44s (0.18s/iter) (5.66 solves/s)
+
+Execution times:
+Wall time (s):	28.17
+CPU time (s):	1.66
+GC time (s):	169.88
+GC overhead (% of CPU time):	10223.84%
+
+GC time per domain (s):
+Domain0: 	0.47
+Domain1: 	9.34
+Domain2: 	6.90
+Domain3: 	6.97
+Domain4: 	6.68
+Domain5: 	6.85
+Domain6: 	6.59
+...
+
+

10223.84% GC overhead sounds like a lot but I think this is a misleading, for a few reasons:

+
    +
  1. The CPU time looks wrong. time reports about 6 minutes, which sounds more likely. +
    2. +
  2. GC time (as we've seen) includes time spent sleeping, while CPU time doesn't. +
    3. +
  3. It doesn't include time spent trying to become a GC leader. +
    4. +
+

To double-check, I modified eio-trace to report GC statistics for a saved trace:

+
Solved 144 requests in 26.84s (0.19s/iter) (5.36 solves/s)
+...
+
+$ eio-trace gc-stats trace.fxt
+./trace.fxt:
+
+Ring  GC/s     App/s    Total/s   %GC
+  0   10.255   19.376   29.631    34.61
+  1    7.986   10.201   18.186    43.91
+  2    8.195   10.648   18.843    43.49
+  3    9.521   14.398   23.919    39.81
+  4    9.775   16.537   26.311    37.15
+  5    8.084   10.635   18.719    43.19
+  6    7.977   10.356   18.333    43.51
+...
+ 24    7.920   10.802   18.722    42.30
+
+All  213.332  308.578  521.910    40.88
+
+Note: all times are wall-clock and so include time spent blocking.
+
+

It ran slightly slower under eio-trace, perhaps because recording a trace file is more work than maintaining some counters, +but it's similar. +So this indicates that with 24 domains GC is taking about 40% of the total time (including time spent sleeping).

+

But something doesn't add up, on my machine at least:

+ +

Even if that 20% were removed completely, it should only save 20% of the 8.2s. +So with domains, the code must be running more slowly even when it's not in the GC.

+

magic-trace on the simple allocator

+

I tried running magic-trace to see what it was doing outside of the GC. +Since it wasn't calling any functions, it didn't show anything, but we can fix that:

+
1
+2
+3
+4
+5
+6
+7
+8
+9
+10
+
let foo () =
+  for _i = 1 to 100 do
+    ignore (Sys.opaque_identity (ref ()))
+  done
+[@@inline never] [@@local never] [@@specialise never]
+
+let run_worker n =
+  for _i = 1 to n * 100000 do
+    foo ()
+  done
+

Here we do blocks of 100 allocations in a function called foo. +The annotations are to ensure the compiler doesn't inline it. +The trace was surprisingly variable!

+

magic-trace of foo between GCs

+

I see times for foo ranging from 50ns to around 750ns!

+

Note: the extra foo call above was probably due to a missed end event somewhere.

+

perf annotate

+

I ran perf record on the simplified version:

+
1
+2
+3
+4
+
let foo () =
+  for _i = 1 to 100 do
+    ignore (Sys.opaque_identity (ref ()))
+  done
+

Here the code is simple enough that we don't need stack-traces (so no -g):

+
$ sudo perf record ./_build/default/main.exe
+$ sudo perf annotate
+
+       │    camlDune__exe__Main.foo_273():
+       │      mov  $0x3,%eax
+  0.04 │      cmp  $0xc9,%rax
+       │    ↓ jg   39
+  7.34 │ d:   sub  $0x10,%r15
+ 13.37 │      cmp  (%r14),%r15
+  0.09 │    ↓ jb   3f
+  0.21 │16:   lea  0x8(%r15),%rbx
+ 70.26 │      movq $0x400,-0x8(%rbx)
+  6.66 │      movq $0x1,(%rbx)
+  0.73 │      mov  %rax,%rbx
+  0.00 │      add  $0x2,%rax
+  0.01 │      cmp  $0xc9,%rbx
+  0.66 │    ↑ jne  d
+  0.28 │39:   mov  $0x1,%eax
+  0.34 │    ← ret
+  0.00 │3f: → call caml_call_gc
+       │    ↑ jmp  16
+
+

The code starts by (pointlessly) checking if 1 > 100 in case it can skip the whole loop. +After being disappointed, it:

+
    +
  1. Decreases %r15 (young_ptr) by 0x10 (two words). +
    2. +
  2. Checks if that's now below young_limit, calling caml_call_gc if so to clear the minor heap. +
    3. +
  3. Writes 0x400 to the first newly-allocated word (the block header, indicating 1 word of data). +
    4. +
  4. Writes 1 to the second word, which represents (). +
    5. +
  5. Increments the loop counter and loops, unless we're at the end. +
    6. +
  6. Returns (). +
    7. +
+

Looks like we spent most of the time (77%) writing the block, which makes sense. +Reading young_limit took 13% of the time, which seems reasonable too. +If there was contention between domains, we'd expect to see it here.

+

The output looked similar whether using domains or processes.

+

perf c2c

+

To double-check, I also tried perf c2c. +This reports on cache-to-cache transfers, where two CPUs are accessing the same memory, +which requires the processors to communicate and is therefore relatively slow.

+
$ sudo perf c2c record
+^C
+
+$ sudo perf c2c report
+  Load Operations                   :      11898
+  Load L1D hit                      :       4140
+  Load L2D hit                      :         93
+  Load LLC hit                      :       3750
+  Load Local HITM                   :        251
+  Store Operations                  :     116386
+  Store L1D Hit                     :     104763
+  Store L1D Miss                    :      11622
+...
+# ----- HITM -----  ------- Store Refs ------  ------- CL --------                      ---------- cycles ----------    Total       cpu                                    Shared                       
+# RmtHitm  LclHitm   L1 Hit  L1 Miss      N/A    Off  Node  PA cnt        Code address  rmt hitm  lcl hitm      load  records       cnt                          Symbol    Object      Source:Line  Node
+...
+      7        0        7        4        0        0      0x7f90b4002b80
+  ----------------------------------------------------------------------
+    0.00%  100.00%    0.00%    0.00%    0.00%    0x0     0       1            0x44a704         0       144       107        8         1  [.] Dune.exe.Main.foo_273       main.exe  main.ml:7        0
+    0.00%    0.00%   25.00%    0.00%    0.00%    0x0     0       1            0x4ba7b9         0         0         0        1         1  [.] caml_interrupt_all_signal_  main.exe  domain.c:318     0
+    0.00%    0.00%   25.00%    0.00%    0.00%    0x0     0       1            0x4ba7e2         0         0       323       49         1  [.] caml_reset_young_limit      main.exe  domain.c:1658    0
+    0.00%    0.00%   25.00%    0.00%    0.00%    0x8     0       1            0x4ce94d         0         0         0        1         1  [.] caml_empty_minor_heap_prom  main.exe  minor_gc.c:622   0
+    0.00%    0.00%   25.00%    0.00%    0.00%    0x8     0       1            0x4ceed2         0         0         0        1         1  [.] caml_alloc_small_dispatch   main.exe  minor_gc.c:874   0
+
+

This shows a list of cache lines (memory addresses) and how often we loaded from a modified address. +There's a lot of information here and I don't understand most of it. +But I think the above is saying that address 0x7f90b4002b80 (young_limit, at offset 0) was accessed by these places across domains:

+ +

The same cacheline was also accessed at offset 8, which contains young_ptr (address of last allocation):

+ +

This indicates false sharing: young_ptr only gets accessed from one domain but it's in the same cache line as young_limit.

+

The main thing is that the counts are all very low, indicating that this doesn't happen often.

+

I tried adding an incr x on a global variable in the loop, and got some more operations reported. +But using Atomic.incr massively increased the number of records:

+
  Original incr Atomic.incr
Load Operations 11,898 25,860 2,658,364
Load L1D hit 4,140 15,181 326,236
Load L2D hit 93 163 295
Load LLC hit 3,750 3,173 2,321,704
Load Local HITM 251 299 2,317,885
Store Operations 116,386 462,162 3,909,500
Store L1D Hit 104,763 389,492 3,908,947
Store L1D Miss 11,622 72,667 550

See C2C - False Sharing Detection in Linux Perf for more information about all this.

+

perf stat

+

perf stat shows statistics about a process. +I ran it with -I 1000 to collect one-second samples. +Here are two samples from the test case on my machine, +one when it was running processes and one while it was using domains:

+
$ perf stat -I 1000
+
+# Processes
+      8,032.71 msec cpu-clock         #    8.033 CPUs utilized
+         2,475      context-switches  #  308.115 /sec
+            51      cpu-migrations    #    6.349 /sec
+            44      page-faults       #    5.478 /sec
+35,268,665,452      cycles            #    4.391 GHz
+48,673,075,188      instructions      #    1.38  insn per cycle
+ 9,815,905,270      branches          #    1.222 G/sec
+    48,986,037      branch-misses     #    0.50% of all branches
+
+# Domains
+      8,008.11 msec cpu-clock         #    8.008 CPUs utilized
+        10,970      context-switches  #    1.370 K/sec
+           133      cpu-migrations    #   16.608 /sec
+           232      page-faults       #   28.971 /sec
+34,606,498,021      cycles            #    4.321 GHz
+25,120,741,129      instructions      #    0.73  insn per cycle
+ 5,028,578,807      branches          #  627.936 M/sec
+    24,402,161      branch-misses     #    0.49% of all branches
+
+

We're doing a lot more context switches with domains, as expected due to the sleeps, +and we're executing many fewer instructions, which isn't surprising. +Reporting the counts for individual CPUs gets more interesting though:

+
$ sudo perf stat -I 1000 -e instructions -Aa
+# Processes
+     1.000409485 CPU0        5,106,261,160      instructions
+     1.000409485 CPU1        2,746,012,554      instructions
+     1.000409485 CPU2       14,235,084,764      instructions
+     1.000409485 CPU3        7,545,940,906      instructions
+     1.000409485 CPU4        2,605,655,333      instructions
+     1.000409485 CPU5        6,023,131,238      instructions
+     1.000409485 CPU6        2,860,656,865      instructions
+     1.000409485 CPU7        8,195,416,048      instructions
+     2.001406580 CPU0        5,674,686,033      instructions
+     2.001406580 CPU1        2,774,756,912      instructions
+     2.001406580 CPU2       12,231,014,682      instructions
+     2.001406580 CPU3        8,292,824,909      instructions
+     2.001406580 CPU4        2,592,461,540      instructions
+     2.001406580 CPU5        7,182,922,668      instructions
+     2.001406580 CPU6        2,742,731,223      instructions
+     2.001406580 CPU7        7,219,186,119      instructions
+     3.002394302 CPU0        4,676,179,731      instructions
+     3.002394302 CPU1        2,773,345,921      instructions
+     3.002394302 CPU2       13,236,080,365      instructions
+     3.002394302 CPU3        5,142,640,767      instructions
+     3.002394302 CPU4        2,580,401,766      instructions
+     3.002394302 CPU5       13,600,129,246      instructions
+     3.002394302 CPU6        2,667,830,277      instructions
+     3.002394302 CPU7        4,908,168,984      instructions
+
+$ sudo perf stat -I 1000 -e instructions -Aa
+# Domains
+     1.002680009 CPU0        3,134,933,139      instructions
+     1.002680009 CPU1        3,140,191,650      instructions
+     1.002680009 CPU2        3,155,579,241      instructions
+     1.002680009 CPU3        3,059,035,269      instructions
+     1.002680009 CPU4        3,102,718,089      instructions
+     1.002680009 CPU5        3,027,660,263      instructions
+     1.002680009 CPU6        3,167,151,483      instructions
+     1.002680009 CPU7        3,214,267,081      instructions
+     2.003692744 CPU0        3,009,806,420      instructions
+     2.003692744 CPU1        3,015,194,636      instructions
+     2.003692744 CPU2        3,093,562,866      instructions
+     2.003692744 CPU3        3,005,546,617      instructions
+     2.003692744 CPU4        3,067,126,726      instructions
+     2.003692744 CPU5        3,042,259,123      instructions
+     2.003692744 CPU6        3,073,514,980      instructions
+     2.003692744 CPU7        3,158,786,841      instructions
+     3.004694851 CPU0        3,069,604,047      instructions
+     3.004694851 CPU1        3,063,976,761      instructions
+     3.004694851 CPU2        3,116,761,158      instructions
+     3.004694851 CPU3        3,045,677,304      instructions
+     3.004694851 CPU4        3,101,053,228      instructions
+     3.004694851 CPU5        2,973,005,489      instructions
+     3.004694851 CPU6        3,109,177,113      instructions
+     3.004694851 CPU7        3,158,349,130      instructions
+
+

In the domains case all CPUs are doing roughly the same amount of work. +But when running separate processes the CPUs differ wildly! +Over the last 1-second interval, for example, CPU5 executed 5.3 times as many instructions as CPU4. +And indeed, some of the test processes are finishing much sooner than the others, +even though they all do the same work.

+

Setting /sys/devices/system/cpu/cpufreq/policy*/energy_performance_preference to performance didn't make it faster, +but setting it to power (power-saving mode) did make the processes benchmark much slower, +while having little effect on the domains case!

+

So I think what's happening here with separate processes is that +the CPU is boosting the performance of one or two cores at a time, +allowing them to make lots of progress.

+

But with domains this doesn't happen, either because no domain runs long enough before sleeping to trigger the boost, +or because as soon as it does it needs to stop and wait for the other domains for a GC and loses it.

+

Conclusions

+

The main profiling and tracing tools used were:

+ +

I think OCaml 5's runtime events tracing was the star of the show here, making it much easier to see what was going on with GC, +especially in combination with perf sched. +statmemprof is also an essential tool for OCaml, and I'll be very glad to get it back with OCaml 5.3. +I think I need to investigate perf more; I'd never used many of these features before. +Though it is important to use it with offcputime etc to check you're not missing samples due to sleeping.

+

Unlike the previous post's example, where the cause was pretty obvious and led to a massive easy speed-up, +this one took a lot of investigation and revealed several problems, none of which seem very easy to fix. +I'm also a lot less confident that I really understand what's happening here, but here is a summary of my current guess:

+ +

Since the sleeping mechanism will be changing in OCaml 5.3, +it would probably be worthwhile checking how that performs too. +I think there are some opportunities to improve the GC, such as letting idle domains opt out of GC after one collection, +and it looks like there are opportunities to reduce the amount of synchronisation done +(e.g. by letting late arrivers start the GC without having to wait for the leader, +or using a lock-free algorithm for becoming leader).

+

For the solver, it would be good to try experimenting with CPU affinity to keep a subset of the 160 cores reserved for the solver. +Increasing the minor heap size and doing work in the main domain should also reduce the overhead of GC, +and improving the version compare function in the opam library would greatly reduce the need for it. +And if my goal was really to make it fast (rather than to improve multicore OCaml and its tooling) +then I'd probably switch it back to using processes.

+

Finally, it was really useful that both of these blog posts examined performance regressions, +so I knew it must be possible to go faster. +Without a good idea of how fast something should be, it's easy to give up too early.

+

Anyway, I hope you found some useful new tool in these posts!

+

Update 2024-08-22

+

I reported above that using chrt to make the process high priority didn't help on my machine. +It also didn't help on the ARM server using the real service. +However, it did help a lot when running the simplified version of the solver on the ARM server!

+

Some more investigation showed that the real service had an additional problem: +it spawned a git log subprocess after every solve, and this was causing all the domains to pause +for about 50ms during the fork operation. +Use OCaml code to find the oldest commit +eliminated the problem (and is also faster, as it can cache the history, although that doesn't matter much).

+

Here are some benchmarks of various combinations of fixes:

+ +

And with that, the new multicore solver service is finally faster than the old process-based one!

+ diff --git a/data/planet/talex5/ocaml-5-performance-problems.md b/data/planet/talex5/ocaml-5-performance-problems.md new file mode 100644 index 0000000000..bbc36aa4a6 --- /dev/null +++ b/data/planet/talex5/ocaml-5-performance-problems.md @@ -0,0 +1,524 @@ +--- +title: OCaml 5 performance problems +description: +url: https://roscidus.com/blog/blog/2024/07/22/performance/ +date: 2024-07-22T10:00:00-00:00 +preview_image: +authors: +- Thomas Leonard +source: +--- + +

Linux and OCaml provide a huge range of tools for investigating performance problems. +In this post I try using some of them to understand a network performance problem. +In part 2, I'll investigate a problem in a CPU-intensive multicore program.

+ +

Table of Contents

+ +

The problem

+

While porting capnp-rpc from Lwt to Eio, +to take advantage of OCaml 5's new effects system, +I tried running the benchmark to see if it got any faster:

+
$ ./echo_bench.exe
+echo_bench.exe: [INFO] rate = 44933.359573 # The old Lwt version
+echo_bench.exe: [INFO] rate = 511.963565   # The (buggy) Eio version
+
+

The benchmark records the number of echo RPCs per second. +Clearly, something is very wrong here! +In fact, the new version was so slow I had to reduce the number of iterations so it would finish.

+

time

+

The old time command can immediately give us a hint:

+
$ /usr/bin/time ./echo_bench.exe
+1.85user 0.42system 0:02.31elapsed 98%CPU  # Lwt
+0.16user 0.05system 0:01.95elapsed 11%CPU  # Eio (buggy)
+
+

(many shells provide their own time built-in with different output formats; I'm using /usr/bin/time here)

+

time's output shows time spent in user-mode (running the application's code on the CPU), +time spent in the kernel, and the total wall-clock time. +Both versions ran for around 2 seconds (doing a different number of iterations), +but the Lwt version was using the CPU 98% of the time, while the Eio version was mostly sleeping.

+

eio-trace

+

eio-trace can be used to see what an Eio program is doing. +Tracing is always available (you don't need to recompile the program to get it).

+
$ eio-trace run -- ./echo_bench.exe
+
+

eio-trace run runs the command and displays the trace in a window. +You can also use eio-trace record to save a trace and examine it later.

+

Trace of slow benchmark (12 concurrent requests)

+

The benchmark runs 12 test clients at once, making it a bit noisy. +To simplify thing, I set it to run only one client:

+

Trace of slow benchmark (one request at a time)

+

I've zoomed the image to show the first four iterations. +The first is so quick it's not really visible, but the next three take about 40ms each. +The yellow regions labelled "suspend-domain" show when the program is sleeping, waiting for an event from Linux. +Each horizontal bar is a fiber (a light-weight thread). From top to bottom they are:

+ +

This trace immediately raises a couple of questions:

+ +

Zooming in on a section between the delays, let's see what it's doing when it's not sleeping:

+

Zoomed in on the active part

+

After a 40ms delay, the server's read fiber receives the next request (the running fiber is shown in green). +The read fiber spawns a fiber to handle the request, which finishes quickly, starts the next read, +and then the write fiber transmits the reply.

+

The client's read fiber gets the reply, the write fiber outputs a message, then the application fiber runs +and another message is sent. +The server reads something (presumably the first message, though it happens after the client had sent both), +then there is another long 40ms delay, then (far off the right of the image) the pattern repeats.

+

To get more context in the trace, +I configured +the logging library to write the (existing) debug-level log messages to the trace buffer too:

+

With log messages

+

Log messages tend to be a bit long for the trace display, so they overlap and you have to zoom right in to read them, +but they do help navigate. +With this, I can see that the first client write is "Send finish" and the second is "Calling Echo.ping".

+

Looks like we're not buffering the output, so it's doing two separate writes rather than combining them. +That's a little inefficient, and if you've done much network programming, +you also probably already know why this might cause a 40ms delay, +but let's pretend we don't know so we can play with a few more tools...

+

strace

+

strace can be used to trace interactions between applications and the Linux kernel +(-tt -T shows when each call was started and how long it took):

+
$ strace -tt -T ./echo_bench.exe
+...
+11:38:58.079200 write(2, "echo_bench.exe: [INFO] Accepting"..., 73) = 73 <0.000008>
+11:38:58.079253 io_uring_enter(4, 4, 0, 0, NULL, 8) = 4 <0.000032>
+11:38:58.079341 io_uring_enter(4, 2, 0, 0, NULL, 8) = 2 <0.000020>
+11:38:58.079408 io_uring_enter(4, 2, 0, 0, NULL, 8) = 2 <0.000021>
+11:38:58.079471 io_uring_enter(4, 2, 0, 0, NULL, 8) = 2 <0.000018>
+11:38:58.079525 io_uring_enter(4, 2, 0, 0, NULL, 8) = 2 <0.000019>
+11:38:58.079580 io_uring_enter(4, 2, 0, 0, NULL, 8) = 2 <0.000013>
+11:38:58.079611 io_uring_enter(4, 1, 0, 0, NULL, 8) = 1 <0.000009>
+11:38:58.079637 io_uring_enter(4, 0, 1, IORING_ENTER_GETEVENTS|IORING_ENTER_EXT_ARG, 0x7ffc1661a480, 24) = -1 ETIME (Timer expired) <0.018913>
+11:38:58.098669 futex(0x5584542b767c, FUTEX_WAKE_PRIVATE, 1) = 1 <0.000105>
+11:38:58.098889 futex(0x5584542b7690, FUTEX_WAKE_PRIVATE, 1) = 1 <0.000059>
+11:38:58.098976 io_uring_enter(4, 0, 1, IORING_ENTER_GETEVENTS, NULL, 8) = 0 <0.021355>
+
+

On Linux, Eio defaults to using the io_uring mechanism for submitting work to the kernel. +io_uring_enter(4, 2, 0, 0, NULL, 8) = 2 means we asked to submit 2 new operations to the ring on FD 4, +and the kernel accepted them.

+

The call at 11:38:58.079637 timed out after 19ms. +It then woke up some futexes and then waited again, getting woken up after a further 21ms (for a total of 40ms).

+

Futexes are used to coordinate between system threads. +strace -f will follow all spawned threads (and processes), not just the main one:

+
$ strace -T -f ./echo_bench.exe
+...
+[pid 48451] newfstatat(AT_FDCWD, "/etc/resolv.conf", {st_mode=S_IFREG|0644, st_size=40, ...}, 0) = 0 <0.000011>
+...
+[pid 48451] futex(0x561def43296c, FUTEX_WAIT_BITSET_PRIVATE|FUTEX_CLOCK_REALTIME, 0, NULL, FUTEX_BITSET_MATCH_ANY <unfinished ...>
+...
+[pid 48449] io_uring_enter(4, 0, 1, IORING_ENTER_GETEVENTS|IORING_ENTER_EXT_ARG, 0x7ffe1d5d1c90, 24) = -1 ETIME (Timer expired) <0.018899>
+[pid 48449] futex(0x561def43296c, FUTEX_WAKE_PRIVATE, 1) = 1 <0.000106>
+[pid 48451] <... futex resumed>)        = 0 <0.019981>
+[pid 48449] io_uring_enter(4, 0, 1, IORING_ENTER_GETEVENTS, NULL, 8 <unfinished ...>
+...
+[pid 48451] exit(0)                     = ?
+[pid 48451] +++ exited with 0 +++
+[pid 48449] <... io_uring_enter resumed>) = 0 <0.021205>
+...
+
+

The benchmark connects to "127.0.0.1" and Eio uses getaddrinfo to look up addresses (we can't use uring for this). +Since getaddrinfo can block for a long time, Eio creates a new system thread (pid 48451) to handle it +(we can guess this thread is doing name resolution because we see it read resolv.conf).

+

As creating system threads is a little slow, Eio keeps the thread around for a bit after it finishes in case it's needed again. +The timeout is when Eio decides that the thread isn't needed any longer and asks it to exit. +So this isn't relevant to our problem (and only happens on the first 40ms delay, since we don't look up any further addresses).

+

However, strace doesn't tell us what the uring operations were, or their return values. +One option is to switch to the posix backend (which is the default on Unix systems). +In fact, it's a good idea with any performance problem to check if it still happens with a different backend:

+
$ EIO_BACKEND=posix strace -T -tt ./echo_bench.exe
+...
+11:53:52.935976 writev(7, [{iov_base="\0\0\0\0\4\0\0\0\0\0\0\0\1\0\1\0\4\0\0\0\0\0\0\0\0\0\0\0\1\0\0\0"..., iov_len=40}], 1) = 40 <0.000170>
+11:53:52.936308 ppoll([{fd=-1}, {fd=-1}, {fd=-1}, {fd=-1}, {fd=4, events=POLLIN}, {fd=-1}, {fd=6, events=POLLIN}, {fd=7, events=POLLIN}, {fd=8, events=POLLIN}], 9, {tv_sec=0, tv_nsec=0}, NULL, 8) = 1 ([{fd=8, revents=POLLIN}], left {tv_sec=0, tv_nsec=0}) <0.000044>
+11:53:52.936500 writev(7, [{iov_base="\0\0\0\0\20\0\0\0\0\0\0\0\1\0\1\0\2\0\0\0\0\0\0\0\0\0\0\0\3\0\3\0"..., iov_len=136}], 1) = 136 <0.000055>
+11:53:52.936831 readv(8, [{iov_base="\0\0\0\0\4\0\0\0\0\0\0\0\1\0\1\0\4\0\0\0\0\0\0\0\0\0\0\0\1\0\0\0"..., iov_len=4096}], 1) = 40 <0.000056>
+11:53:52.937516 ppoll([{fd=-1}, {fd=-1}, {fd=-1}, {fd=-1}, {fd=4, events=POLLIN}, {fd=-1}, {fd=6, events=POLLIN}, {fd=7, events=POLLIN}, {fd=8, events=POLLIN}], 9, NULL, NULL, 8) = 1 ([{fd=8, revents=POLLIN}]) <0.038972>
+11:53:52.977751 readv(8, [{iov_base="\0\0\0\0\20\0\0\0\0\0\0\0\1\0\1\0\2\0\0\0\0\0\0\0\0\0\0\0\3\0\3\0"..., iov_len=4096}], 1) = 136 <0.000398>
+
+

(to reduce clutter, I removed calls that returned EAGAIN and ppoll calls that returned 0 ready descriptors)

+

The problem still occurs, and now we can see the two writes:

+ +

bpftrace

+

Alternatively, we can trace uring operations using bpftrace. +bpftrace is a little scripting language similar to awk, +except that instead of editing a stream of characters, +it live-patches the running Linux kernel. +Apparently this is safe to run in production +(and I haven't managed to crash my kernel with it yet).

+

Here is a list of uring tracepoints we can probe:

+
$ sudo bpftrace -l 'tracepoint:io_uring:*'
+tracepoint:io_uring:io_uring_complete
+tracepoint:io_uring:io_uring_cqe_overflow
+tracepoint:io_uring:io_uring_cqring_wait
+tracepoint:io_uring:io_uring_create
+tracepoint:io_uring:io_uring_defer
+tracepoint:io_uring:io_uring_fail_link
+tracepoint:io_uring:io_uring_file_get
+tracepoint:io_uring:io_uring_link
+tracepoint:io_uring:io_uring_local_work_run
+tracepoint:io_uring:io_uring_poll_arm
+tracepoint:io_uring:io_uring_queue_async_work
+tracepoint:io_uring:io_uring_register
+tracepoint:io_uring:io_uring_req_failed
+tracepoint:io_uring:io_uring_short_write
+tracepoint:io_uring:io_uring_submit_req
+tracepoint:io_uring:io_uring_task_add
+tracepoint:io_uring:io_uring_task_work_run
+
+

io_uring_complete looks promising:

+
$ sudo bpftrace -vl tracepoint:io_uring:io_uring_complete
+tracepoint:io_uring:io_uring_complete
+    void * ctx
+    void * req
+    u64 user_data
+    int res
+    unsigned cflags
+    u64 extra1
+    u64 extra2
+
+

Here's a script to print out the time, process, operation name and result for each completion:

+
uringtrace.bt
1
+2
+3
+4
+5
+6
+7
+8
+9
+10
+11
+12
+13
+14
+15
+16
+17
+18
+
BEGIN {
+  @op[IORING_OP_NOP] = "NOP";
+  @op[IORING_OP_READV] = "READV";
+  ...
+}
+
+tracepoint:io_uring:io_uring_complete {
+  $req = (struct io_kiocb *) args->req;
+  printf("%dms: %s: %s %d\n",
+    elapsed / 1e6,
+    comm,
+    @op[$req->opcode],
+    args->res);
+}
+
+END {
+  clear(@op);
+}
+
$ sudo bpftrace uringtrace.bt
+Attaching 3 probes...
+...
+1743ms: echo_bench.exe: WRITE_FIXED 40
+1743ms: echo_bench.exe: READV 40
+1743ms: echo_bench.exe: WRITE_FIXED 136
+1783ms: echo_bench.exe: READV 136
+
+

In this output, the order is slightly different: +we see the server's read get the 40 bytes before the client sends the rest, +but we still see the 40ms delay between the completion of the second write and the corresponding read. +The change in order is because we're seeing when the kernel knew the read was complete, +not when the application found out about it.

+

tcpdump

+

An obvious step with any networking problem is the look at the packets going over the network. +tcpdump can be used to capture packets, which can be displayed on the console or in a GUI with wireshark.

+
$ sudo tcpdump -n -ttttt -i lo
+...
+...041330 IP ...37640 > ...7000: Flags [P.], ..., length 40
+...081975 IP ...7000 > ...37640: Flags [.], ..., length 0
+...082005 IP ...37640 > ...7000: Flags [P.], ..., length 136
+...082071 IP ...7000 > ...37640: Flags [.], ..., length 0
+
+

Here we see the client (on port 37640) sending 40 bytes to the server (port 7000), +and the server replying with an ACK (with no payload) 40ms later. +After getting the ACK, the client socket sends the remaining 136 bytes.

+

Here we can see that while the application made the two writes in quick succession, +TCP waited before sending the second one. +Searching for "delayed ack 40ms" will turn up an explanation.

+

ss

+

ss displays socket statistics. +ss -tin shows all TCP sockets (-t) with internals (-i):

+
$ ss -tin 'sport = 7000 or dport = 7000'
+State   Recv-Q   Send-Q  Local Address:Port  Peer Address:Port
+ESTAB   0        0       127.0.0.1:7000      127.0.0.1:56224
+ ato:40 lastsnd:34 lastrcv:34 lastack:34
+ESTAB   0        176     127.0.0.1:56224     127.0.0.1:7000
+ ato:40 lastsnd:34 lastrcv:34 lastack:34 unacked:1 notsent:136
+
+

There's a lot of output here; I've removed the irrelevant bits. +ato:40 says there's a 40ms timeout for "delay ack mode". +lastsnd, etc, say that nothing had happened for 34ms when this information was collected. +unacked and notsent aren't documented in the man-page, +but I guess it means that the client (now port 56224) is waiting for 1 packet to be ack'd and has 136 bytes waiting until then.

+

The client socket still has both messages (176 bytes total) in its queue; +it can't forget about the first message until the server confirms receiving it, +since the client might need to send it again if it got lost.

+

This doesn't quite lead us to the solution, though.

+

offwaketime

+

offwaketime records why a program stopped using the CPU, and what caused it to resume:

+
$ sudo offwaketime-bpfcc -f -p (pgrep echo_bench.exe) > wakes
+$ flamegraph.pl --colors=chain wakes > wakes.svg
+
+

Time spent suspended along with wakeup reason

+

offwaketime records a stack-trace when a process is suspended (shown at the bottom and going up) +and pairs it with the stack-trace of the thread that caused it to be resumed (shown above it and going down).

+

The taller column on the right shows Eio being woken up due to TCP data being received from the network, +confirming that it was the TCP ACK that got things going again.

+

The shorter column on the left was unexpected, and the [UNKNOWN] in the stack is annoying +(probably C code compiled without frame pointers). +gdb gets a better stack trace. +It turned out to be OCaml's tick thread, which wakes every 50ms to prevent one sys-thread from hogging the CPU:

+
$ strace -T -e pselect6 -p (pgrep echo_bench.exe) -f
+strace: Process 20162 attached with 2 threads
+...
+[pid 20173] pselect6(0, NULL, NULL, NULL, {tv_sec=0, tv_nsec=50000000}, NULL) = 0 (Timeout) <0.050441>
+[pid 20173] pselect6(0, NULL, NULL, NULL, {tv_sec=0, tv_nsec=50000000}, NULL) = 0 (Timeout) <0.050318>
+
+

Having multiple threads shown on the same diagram is a bit confusing. +I should probably have used -t to focus only on the main one.

+

Also, note that when using profiling tools that record the OCaml stack, +it's useful to compile with frame pointers enabled. +To install e.g. OCaml 5.2.0 with frame pointers enabled, use:

+
1
+
$ opam switch create 5.2.0-fp ocaml-variants.5.2.0+options ocaml-option-fp
+

magic-trace

+

magic-trace allows capturing a short trace of everything the CPUs were doing just before some event. +It uses Intel Processor Trace to have the CPU record all control flow changes (calls, branches, etc) to a ring-buffer, +with fairly low overhead (2% to 10%, due to extra memory bandwidth needed). +When something interesting happens, we save the buffer and use it to reconstruct the recent history.

+

Normally we'd need to set up a trigger to grab the buffer at the right moment, +but since this program is mostly idle it doesn't record much +and I just attached at a random point and immediately pressed Ctrl-C to grab a snapshot and detach:

+
1
+2
+3
+4
+
$ sudo magic-trace attach -multi-thread -trace-include-kernel \
+    -p (pgrep echo_bench.exe)
+[ Attached. Press Ctrl-C to stop recording. ]
+^C
+

As before, we see 40ms periods of waiting, with bursts of activity between them:

+

Magic trace showing 40ms delays

+

The output is a bit messed up because magic-trace doesn't understand that there are multiple OCaml fibers here, +each with their own stack. It also doesn't seem to know that exceptions unwind the stack.

+

In each 40ms column, Eio_posix.Flow.single_read (3rd line from top) tried to do a read +with readv, which got EAGAIN and called Sched.next to switch to the next fiber. +Since there was nothing left to run, the Eio scheduler called ppoll. +Linux didn't have anything ready for this process, +and called the schedule kernel function to switch to another process.

+

I recorded an eio-trace at the same time, to see the bigger picture. +Here's the eio-trace zoomed in to show the two client writes (just before the 40ms wait), +with the relevant bits of the magic-trace stack pasted below them:

+

Zoomed in on the two client writes, showing eio-trace and magic-trace output together

+

We can see the OCaml code calling writev, entering the kernel, tcp_write_xmit being called to handle it, +writing the IP packet to the network and then, because this is the loopback interface, the network receive logic +handling the packet too. +The second call is much shorter; tcp_write_xmit returns quickly without sending anything.

+

Note: I used the eio_posix backend here so it's easier to correlate the kernel operations to the application calls +(uring queues them up and runs them later). +The uring-trace project should make this easier in future, but doesn't integrate with eio-trace yet.

+

Zooming in further, it's easy to see the difference between the two calls to tcp_write_xmit:

+

The start of the first tcp_write_xmit and the whole of the second +Looking at the source for tcp_write_xmit, +we finally find the magic word "nagle"!

+
1
+2
+3
+4
+
if (unlikely(!tcp_nagle_test(tp, skb, mss_now,
+			     (tcp_skb_is_last(sk, skb) ?
+			      nonagle : TCP_NAGLE_PUSH))))
+	break;
+

Summary script

+

Having identified a load of interesting events +I wrote summary-posix.bt, a bpftrace script to summarise them. +This includes log messages written by the application (by tracing write calls to stderr), +reads and writes on the sockets, +and various probed kernel functions seen in the magic-trace output and when reading the kernel source.

+

The output is specialised to this application (for example, TCP segments sent to port 7000 +are displayed as "to server", while others are "to client"). +I think this is a useful way to double-check my understanding, and any fix:

+
$ sudo bpftrace summary-posix.bt
+[...]
+844ms: server: got ping request; sending reply
+844ms: server reads from socket (EAGAIN)
+844ms: server: writev(96 bytes)
+844ms:   tcp_write_xmit (to client, nagle-on, packets_out=0)
+844ms:   tcp_v4_send_check: sending 96 bytes to client
+844ms: tcp_v4_rcv: got 96 bytes
+844ms:   timer_start (tcp_delack_timer, 40 ms)
+844ms: client reads 96 bytes from socket
+844ms: client: enqueue finish message
+844ms: client: enqueue ping call
+844ms: client reads from socket (EAGAIN)
+844ms: client: writev(40 bytes)
+844ms:   tcp_write_xmit (to server, nagle-on, packets_out=0)
+844ms:   tcp_v4_send_check: sending 40 bytes to server
+845ms: tcp_v4_rcv: got 40 bytes
+845ms:   timer_start (tcp_delack_timer, 40 ms)
+845ms: client: writev(136 bytes)
+845ms:   tcp_write_xmit (to server, nagle-on, packets_out=1)
+845ms: server reads 40 bytes from socket
+845ms: server reads from socket (EAGAIN)
+885ms: tcp_delack_timer_handler (ACK to client)
+885ms:   tcp_v4_send_check: sending 0 bytes to client
+885ms: tcp_delack_timer_handler (ACK to server)
+885ms: tcp_v4_rcv: got 0 bytes
+885ms:   tcp_write_xmit (to server, nagle-on, packets_out=0)
+885ms:   tcp_v4_send_check: sending 136 bytes to server
+
+
    +
  1. The server replies to a ping request, sending a 96 byte reply. +Nagle is on, but nothing is awaiting an ACK (packets_out=0) so it gets sent immediately. +
    2. +
  2. The client receives the data. It starts a 40ms timer to send an ACK for it. +
    3. +
  3. The client enqueues a "finish" message, followed by another "ping" request. +
    4. +
  4. The client's write fiber sends the 40 byte "finish" message. +Nothing is awaiting an ACK (packets_out=0) so the kernel sends it immediately. +
    5. +
  5. The client sends the 136 byte ping request. As the last message hasn't been ACK'd, it isn't sent yet. +
    6. +
  6. The server receives the 40 byte finish message. +
    7. +
  7. 40ms pass. The server's delayed ACK timer fires and it sends the ACK to the client. +
    8. +
  8. The client's delayed ACK timer fires, but there's nothing to do (it sent the ACK with the "finish"). +
    9. +
  9. The client socket gets the ACK for its "finish" message and sends the delayed ping request. +
    10. +
+

Fixing it

+

The problem seemed clear: while porting from Lwt to Eio I'd lost the output buffering. +So I looked at the Lwt code to see how it did it and... it doesn't! So how was it working?

+

As I did with Eio, I set the Lwt benchmark's concurrency to 1 to simplify it for tracing, +and discovered that Lwt with 1 client thread has exactly the same problem as the Eio version. +Well, that's embarrassing! +But why is Lwt fast with 12 client threads?

+

With only minor changes (e.g. write vs writev), the summary script above also worked for tracing the Lwt version. +With 1 or 2 client threads, Lwt is slow, but with 3 it's fairly fast. +The delay only happens if the client sends a "finish" message when the server has no replies queued up +(otherwise the finish message unblocks the replies, which carry the ACK to the client immediately). +So, it works mostly by fluke! +Lwt just happens to schedule the threads in such a way that Nagle's algorithm mostly doesn't trigger with 12 concurrent requests.

+

Anyway, adding buffering to the Eio version fixed the problem:

+

Before +After (same scale)

+

An interesting thing to notice here is that not only did the long delay go away, +but the CPU operations while it was active were faster too! +I think the reason is that the CPU goes into power-saving mode during the long delays. +cpupower monitor shows my CPUs running at around 1 GHz with the old code and +around 4.7 GHz when running the new version.

+

Here are the results for the fixed version:

+
$ ./echo_bench.exe
+echo_bench.exe: [INFO] rate = 44425.962625 # The old Lwt version
+echo_bench.exe: [INFO] rate = 59653.451934 # The fixed Eio version
+
+

60k RPC requests per second doesn't seem that impressive, but at least it's faster than the old version, +which is good enough for now! There's clearly scope for improvement here (for example, the buffering I +added is quite inefficient, making two extra copies of every message, as the framing library copies it from +a cstruct to a string, and then I have to copy the string back to a cstruct for the kernel).

+

Conclusions

+

There are lots of great tools available to help understand why something is running slowly (or misbehaving), +and since programmers usually don't have much time for profiling, +a little investigation will often turn up something interesting! +Even when things are working correctly, these tools are a good way to learn more about how things work.

+

time will quickly tell you if the program is taking lots of time in application code, in the kernel, or just sleeping. +If the problem is sleeping, offcputime and offwaketime can tell you why it was waiting and what woke it in the end. +My own eio-trace tool will give a quick visual overview of what an Eio application is doing. +strace is great for tracing interactions between applications and the kernel, +but it doesn't help much when the application is using uring. +To fix that, you can either switch to the eio_posix backend or use bpftrace with the uring tracepoints. +tcpdump, wireshark and ss are all useful to examine network problems specifically.

+

I've found bpftrace to be really useful for all kinds of tasks. +Being able to write quick one-liners or short scripts gives it great flexibility. +Since the scripts run in the kernel you can also filter and aggregate data efficiently +without having to pass it all to userspace, and you can examine any kernel data structures. +We didn't need that here because the program was running so slowly, but it's great for many problems. +In addition to using well-defined tracepoints, +it can also probe any (non-inlined) function in the kernel or the application. +I also think using it to create a "summary script" to confirm a problem and its solution seems useful, +though this is the first time I've tried doing that.

+

magic-trace is great for getting really detailed function-by-function tracing through the application and kernel. +Its ability to report the last few ms of activity after you notice a problem is extremely useful +(though not needed in this example). +It would be really useful if you could trigger magic-trace from a bpftrace script, but I didn't see a way to do that.

+

However, it was surprisingly difficult to get any of the tools to point directly +at the combination of Nagle's algorithm with delayed ACKs as the cause of this common problem!

+

This post was mainly focused on what was happening in the kernel. +In part 2, I'll investigate a CPU-intensive problem instead.

+ diff --git a/data/planet/tarides/creating-the-syntaxdocumentation-command---part-3-vscode-platform-extension.md b/data/planet/tarides/creating-the-syntaxdocumentation-command---part-3-vscode-platform-extension.md new file mode 100644 index 0000000000..3212e05f55 --- /dev/null +++ b/data/planet/tarides/creating-the-syntaxdocumentation-command---part-3-vscode-platform-extension.md @@ -0,0 +1,197 @@ +--- +title: 'Creating the SyntaxDocumentation Command - Part 3: VSCode Platform Extension' +description: Discover how `SyntaxDocumentation` became an opt-in feature within the + OCaml VSCode Platform extension, enhancing configuration in the VSCode editor. +url: https://tarides.com/blog/2024-07-24-creating-the-syntaxdocumentation-command-part-3-vscode-platform-extension +date: 2024-07-24T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/vscode_toggle-1360w.webp +authors: +- Tarides +source: +--- + +

In the final installment of our series on the SyntaxDocumentation command, we delve into its integration within the OCaml VSCode Platform extension. Building on our previous discussions about Merlin and OCaml LSP, this article explores how to make SyntaxDocumentation an opt-in feature in the popular VSCode editor.

+

In the first part of this series, Creating the SyntaxDocumentation Command - Part 1: Merlin, we explored how to create a new command in Merlin, particularly the SyntaxDocumentation command. In the second part, Creating the SyntaxDocumentation Command - Part 2: OCaml LSP, we looked at how to implement this feature in OCaml LSP in order to enable visual editors to trigger the command with actions such as hovering. In this third and final installment, you will learn how SyntaxDocumentation integrates into the OCaml VSCode Platform extension as an opt-in feature, enabling users to toggle it on/off depending on their preference.

+

VSCode Editor

+

Visual Studio Code is a free open-source, cross-platform code editor from Microsoft that is very popular among developers. +Some of its features include:

+ +

OCaml Platform Extension for VSCode

+

The VSCode OCaml Platform extension enhances the development experience for OCaml programmers. It is itself written in the OCaml programming language using bindings to the VSCode API and then compiled into Javascript with js_of_ocaml. It provides language support features such as syntax-highlighting, go-to-definition, auto-completion, and type-on-hover. These key functionalities are powered by the OCaml Language Server (ocamllsp), which can be installed using popular package managers like opam and esy. Users can easily configure the extension to work with different sandbox environments, ensuring a tailored setup for various project needs. Additionally, the extension includes comprehensive settings and command options, making it very versatile for both beginner and advanced OCaml developers.

+

The OCaml Platform Extension for VSCode gives us a nice UI for interacting with OCaml-LSP. We can configure settings for the server as well as interact with switches, browse the AST, and many more features. Our main focus is on adding a checkbox that allows users to activate or deactivate SyntaxDocumentation in OCaml LSP's hover response. I limited this article's scope to just the files relevant in implementing this, while giving a brief tour of how the extension is built.

+

The Implementation

+

Extension Manifest

+

Every VSCode extension has a manifest file, package.json, at the root of the extension directory. The package.json contains a mix of Node.js fields, such as scripts and devDependencies, and VS Code specific fields, like publisher, activationEvents, and contributes. +Our manifest file contains general information such as:

+ +

We also have commands that act as action events for our extension. These commands are used to perform a wide range of things, like navigating the AST, upgrading packages, deleting a switch, etc. +An example of a command to open the AST explorer is written as:

+
{
+    "command": "ocaml.open-ast-explorer-to-the-side",
+    "category": "OCaml",
+    "title": "Open AST explorer"
+}
+
+

For our case, enabling/disabling SyntaxDocumentation is a configuration setting for our language server, so we indicate this in the configurations section:

+
"ocaml.server.syntaxDocumentation": {
+    "type": "boolean",
+    "default": false,
+    "markdownDescription": "Enable/Disable syntax documentation"
+}
+
+

Extension Instance

+

The file extension_instance.ml handles the setup and configuration of various components of the OCaml VSCode extension and ensures that features like the language server and documentation are properly initialised. Its key functionalities are:

+ +
type t = {
+  mutable sandbox : Sandbox.t;
+  mutable repl : Terminal_sandbox.t option;
+  mutable ocaml_version : Ocaml_version.t option;
+  mutable lsp_client : (LanguageClient.t * Ocaml_lsp.t) option;
+  mutable documentation_server : Documentation_server.t option;
+  documentation_server_info : StatusBarItem.t;
+  sandbox_info : StatusBarItem.t;
+  ast_editor_state : Ast_editor_state.t;
+  mutable codelens : bool option;
+  mutable extended_hover : bool option;
+  mutable dune_diagnostics : bool option;
+  mutable syntax_documentation : bool option;
+}
+
+ +
...
+
+(* Set configuration *)
+let set_configuration t ~syntax_documentation =
+  t.syntax_documentation <- syntax_documentation;
+  match t.lsp_client with
+  | None -> ()
+  | Some (client, (_ : Ocaml_lsp.t)) ->
+      send_configuration ~syntax_documentation client
+...
+
+
...
+
+(* Send configuration *)
+let send_configuration ~syntax_documentation client =
+  let syntaxDocumentation =
+    Option.map syntax_documentation ~f:(fun enable ->
+        Ocaml_lsp.OcamllspSettingEnable.create ~enable)
+  in
+  let settings =
+    Ocaml_lsp.OcamllspSettings.create
+      ~syntaxDocumentation
+  in
+  let payload =
+    let settings =
+      LanguageClient.DidChangeConfiguration.create
+        ~settings:(Ocaml_lsp.OcamllspSettings.t_to_js settings)
+        ()
+    in
+    LanguageClient.DidChangeConfiguration.t_to_js settings
+  in
+  LanguageClient.sendNotification
+    client
+    "workspace/didChangeConfiguration"
+    payload
+
+...
+
+

Interacting With OCaml LSP:

+

The ocaml_lsp.ml file ensures that ocamllsp is set up correctly and up to date. For SyntaxDocumentation, two important modules used from this file are: OcamllspSettingEnable and OcamllspSettings.

+

OcamllspSettingEnable defines an interface for enabling/disabling specific settings in ocamllsp.

+
...
+
+module OcamllspSettingEnable = struct
+  include Interface.Make ()
+  include
+    [%js:
+    val enable : t -> bool or_undefined [@@js.get]
+    val create : enable:bool -> t [@@js.builder]]
+end
+
+...
+
+

The annotation [@@js.get] is a PPX used to bind OCaml functions to JavaScript property accessors. This allows OCaml code to interact seamlessly with JavaScript objects, accessing properties directly as if they were native OCaml fields, while [@@js.builder] facilitates the creation of JavaScript objects from OCaml functions. They both come from the LexFi/gen_js_api library.

+

OcamllspSettings aggregrates multiple OcamllspSettingEnable settings into a comprehensive settings interface for ocamllsp.

+
...
+module OcamllspSettings = struct
+  include Interface.Make ()
+  include
+    [%js:
+    val syntaxDocumentation : t ->
+      OcamllspSettingEnable.t or_undefined [@@js.get]
+
+    val create : ?syntaxDocumentation:OcamllspSettingEnable.t ->
+      unit -> t [@@js.builder]]
+
+  let create ~syntaxDocumentation = create ?syntaxDocumentation ()
+end
+...
+
+

Workspace Configuration

+

The file settings.ml provides a flexible way to manage workspace-specific settings, including:

+ +
...
+let create_setting ~scope ~key ~of_json ~to_json =
+  { scope; key; to_json; of_json }
+
+let server_syntaxDocumentation_setting =
+  create_setting
+    ~scope:ConfigurationTarget.Workspace
+    ~key:"ocaml.server.syntaxDocumentation"
+    ~of_json:Jsonoo.Decode.bool
+    ~to_json:Jsonoo.Encode.bool
+...
+
+

Activating the Extension

+

The vscode_ocaml_platform.ml file initialises and activates the OCaml Platform extension for VSCode. The key tasks include:

+ +

In the context of SyntaxDocumentation, this code ensures that the extension is correctly configured to handle SyntaxDocumentation settings. The notify_configuration_changes function listens for changes to the server_syntaxDocumentation_setting and updates the extension instance accordingly. This means that any changes the user makes to the SyntaxDocumentation settings in the VSCode workspace configuration will be reflected in the extension's behaviour, ensuring that SyntaxDocumentation is enabled or disabled as per the user's preference.

+
let notify_configuration_changes instance =
+  Workspace.onDidChangeConfiguration
+    ~listener:(fun _event ->
+      let syntax_documentation =
+        Settings.(get server_syntaxDocumentation_setting)
+      in
+      Extension_instance.set_configuration instance ~syntax_documentation)
+    ()
+
+

Conclusion

+

SyntaxDocument toggle

+

In this final article, we explored how to integrate SyntaxDocumentation into OCaml VSCode Platform extension as a configurable option for OCaml LSP's hover command. We covered key components such as configuring the extension manifest, managing the extension state, interacting with the OCaml language server, and handling workspace configurations. By enabling users to toggle the SyntaxDocumentation feature on or off, we can ensure a flexible and customisable development experience for all users.

+

Feel free to contribute to this extension on the GitHub repository: vscode-ocaml-platform. Thank you for following along in this series, and happy coding with OCaml and VSCode!

+ diff --git a/data/planet/tarides/deep-dive-optimising-multicore-ocaml-for-windows.md b/data/planet/tarides/deep-dive-optimising-multicore-ocaml-for-windows.md new file mode 100644 index 0000000000..bf5e790941 --- /dev/null +++ b/data/planet/tarides/deep-dive-optimising-multicore-ocaml-for-windows.md @@ -0,0 +1,53 @@ +--- +title: 'Deep Dive: Optimising Multicore OCaml for Windows' +description: Intern tackled OCaml's multicore performance drop on Windows, optimizing + busy-wait loops with barriers and futexes, enhancing runtime efficiency across OS. +url: https://tarides.com/blog/2024-07-10-deep-dive-optimising-multicore-ocaml-for-windows +date: 2024-07-10T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/racecar-1360w.webp +authors: +- Tarides +source: +--- + +

We love hosting internships. It is rewarding to potentially facilitate someone’s first foray into the OCaml ecosystem, helping them establish a hopefully life-long foothold in the world of open-source programming. It is also a great opportunity to get new perspectives on existing issues. Fresh eyes can reinvigorate topics, highlighting different pain points and new solutions which benefit the entire community.

+

Sometimes, we also find ourselves just trying to keep up with our interns as they take off like rocket ships! Recently, we mentored a student who did just that. The initial goal of the internship was to investigate strange performance drops in the OCaml runtime that arose after the introduction of multicore support. These performance drops were most keenly felt on Windows machines, and the initial internship specification emphasised the need to improve the developer experience on that operating system.

+

Our intern @eutro went above and beyond anything we could have expected and tackled the project thoroughly and ambitiously. In this post, I will attempt to give you a comprehensive overview of this intricate project and the problems it tackled.

+

Get Busy Waiting?

+

Before OCaml 5, only one thread would run at any given time. Users never had to worry about multiple threads trying to use a shared resource like the Garbage Collector (GC). In OCaml 5, however, the process is divided into several 'threads'[1], and multiple threads regularly try to run parts of the GC simultaneously. The minor GC uses a Stop The World (STW) function to run in parallel on all threads, whereas the major GC’s work is split into slices. These may happen in parallel between threads and while the user’s program (also called the ‘mutator’) is making changes. This is one example of when a mechanism is needed to protect multiple threads from making changes that contradict each other and result in unexpected behaviours.

+

Locks are the traditional way of doing this, whereby other activity is halted (or locked) while one activity finishes. However, in multicore programming, this method would be incredibly inefficient since there can be many activities in progress simultaneously. In this case, we would need to introduce so many locks for the different parts of memory that doing so would cause memory and OS resource problems!

+

The approach we use for OCaml 5 combines a Compare And Swap (CAS) operation with Busy-Wait loops. A CAS operation ensures that if two threads try to modify the same area of memory, only one will succeed. The one that fails will know it has failed and can then enter a period of Busy-Waiting (called SPIN_WAIT in the code). Busy-wait loops (also referred to as spins) describe a process that repeatedly ('busily') checks whether a condition is true. The process or task is only resumed once that condition is met.

+

Sleeping Beauty

+

Busy-wait loops are used successfully in OCaml for many purposes but have been optimised. They are mostly appropriate in cases where we think that the required condition will be met quickly or in a reasonable period of time. If that’s not the case, then theoretically, the thread that is waiting will just keep spinning. If one allows busy-wait loops to spin indefinitely, they waste a lot of power and CPU and can actually prevent the condition they are waiting for from being met. To avoid that happening, we can use a sleep function.

+

In order to implement spinning without wasting power, the loop checks the condition repeatedly, but after a while, it starts 'sleeping' between checks. Suppose a thread is waiting for condition C to come true, and it uses a Busy-Wait loop to check for this. The program spins a number of times, checking the condition, and then waits or goes to ‘sleep’ for a set amount of time – then it ‘wakes up’ and checks once more before (if it has to) going back to ‘sleep‘ again. The period of ‘sleep’ increases each time. This cycle repeats itself until the condition C finally comes true.

+

This was how the process was supposed to work, yet, for some unknown reason, certain processes would occasionally take much longer than expected. The performance drop was worst on Windows machines.

+

Testing 1-2-3, Testing 1-2-3,

+

The first order of business was to conduct a series of tests on the runtime. Not only to discover the possible cause of the performance drops but also to establish a baseline of performance against which to measure any changes (and hopefully improvements!).

+

We knew that there was a performance problem and that it was particularly painful on Windows, but we didn’t know why. Even if we had a hunch as to what might be causing it, it was crucial to build up a realistic image of what was happening before we attempted a fix.

+

@eutro began this process by identifying where Busy-Wait loops were spinning in the runtime and for how long. She also wanted to know if there were places in the runtime where processes would get ‘stuck’ in Busy-Wait loops and not move on, and if so, where and why.

+

She used the OCaml testsuite and measured how many SPIN_WAIT macros resolved successfully without needing to sleep and which ones did not. She discovered that in most cases, the spinning had the desired effect, and the process could continue after a reasonable amount of time when the condition it was waiting for was met. The garbage collector was also not experiencing any significant performance drops, so it could not be the cause of the problems on Windows. Instead, what she realised was that on Windows, sleeps cannot be shorter than one millisecond, and so the first sleeps that occur end up being much too long. This causes extended and unnecessary delays for processes running on Windows. Equipped with this realisation, @eutro got started on a solution. One that would be most helpful on Windows but still benefit users on other operating systems.

+

Barriers and Futexes, Oh My!

+

There are a few ways a thread in OCaml can wait for a condition:

+ +

So what has changed? As things stood, only steps one and two were available, a series of increasingly long sleeps interleaved with checks. So you would spin n times, then sleep for 10µs (‘µs’ is short for microseconds), then you check the condition once more and might sleep for 20µs, then 35µs, and so on. The point is that the time spent sleeping kept gradually increasing.

+

However, as @eutro discovered, in many cases, the process took far too long to resume, even after the condition had come true. By the time they woke up from sleeping, they could have already proceeded if they had just ‘taken a ticket’ earlier and waited until they were notified. To improve performance, instead of repeatedly sleeping for longer increments, we use specialised ‘barriers’ to wait until we can proceed.

+

To solve the Windows problem, we now use the SPIN_WAIT function only in cases where we don’t expect to ever need to sleep. In cases where that first sleep would cause significant delay, we introduce a new SPIN_WAIT_NTIMES function, which lets the process spin for a set number of times before being combined with a barrier. @eutro used her previous benchmarks to determine which occasions could keep the SPIN_WAIT cycle as-is and which occasions required the new SPIN_WAIT_NTIMES combined with a barrier.

+

But things didn’t stop there! @eutro could also optimise the type of barrier. Traditionally, we use condition variables to wake up threads waiting on a condition. However, they are unnecessarily resource-intensive as they require extra memory, and since woken threads must acquire (and release) a lock before they continue. A futex is a lower-level synchronisation primitive that can similarly be used to wake up threads but without the added complexity of a condition variable.

+

@eutro added the use of futexes to the operating systems that permitted her to do so. Notably, macOS does not allow non-OS programs to use futexes so we fall back to using "condition variables" there.

+

By introducing the use of SPIN_WAIT_NTIMES, barriers, and futexes, @eutro implemented a number of optimisations that were applicable not only on Windows but on several operating systems. These optimisations save users time and processing power.

+

How Much do You Bench(mark)?

+

During the course of implementing these changes, @eutro did a lot of tests. It was important to be thorough in order to ensure that her changes didn’t have unintended consequences. It is incredibly difficult to reason about how programs will react to a specific alteration, as there are many things happening in the runtime and several ways that programs can interact.

+

She used the OCaml test suite again, this time to help her check that the OCaml runtime and other OCaml programs functioned correctly. Having verified that they were, @eutro also ran several benchmarks to check that she hadn’t actually made anything slower. For this, she used the Sandmark test suite.

+

I recommend checking out the tests and benchmarks for yourself in the Pull Request. The PR also gives a more in-depth technical overview of the changes to the Busy-Waiting loops.

+

You Can Join Us Too!

+

It is great to see what someone with a passion for OCaml can bring to the system as a whole. I think it illustrates the benefits of open-source software development: when we invite fresh observations and suggestions, we create a community that supports innovation and collaboration. We are impressed with the hard work @eutro put into solving the complicated problem before her. She went above and beyond what we thought possible in such a short amount of time!

+

Would you like to complete an internship with us? We welcome people of varying experience levels – some interns have made open-source contributions before and are familiar with functional programming, and some of our interns have no functional programming experience at all! If you’re interested in developing your skills in a supportive environment, keep an eye on our careers page, where we post about any available internships. We also regularly communicate about available internships on X (formerly known as Twitter). We hope to hear from you!

+
    +
  1. +

    We are aware of the distinction between ‘threads’ and ‘domains’ in OCaml. We chose to use the former here, mainly to keep the content accessible for people who are less familiar with the subtleties of OCaml.

    +↩︎︎
+ diff --git a/data/planet/tarides/dune-developer-preview-installing-the-ocaml-compiler-with-dune-package-management.md b/data/planet/tarides/dune-developer-preview-installing-the-ocaml-compiler-with-dune-package-management.md new file mode 100644 index 0000000000..318a199e20 --- /dev/null +++ b/data/planet/tarides/dune-developer-preview-installing-the-ocaml-compiler-with-dune-package-management.md @@ -0,0 +1,21 @@ +--- +title: 'Dune Developer Preview: Installing The OCaml Compiler With Dune Package Management' +description: Dune's Package Management now supports direct installation of OCaml compilers, + streamlining setup and enabling shared usage across projects for faster builds. +url: https://tarides.com/blog/2024-10-16-dune-developer-preview-installing-the-ocaml-compiler-with-dune-package-management +date: 2024-10-16T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/enhancing_dune-1360w.webp +authors: +- Tarides +source: +--- + +

We’re excited to share a significant update to Dune's Package Management system, particularly one that will be of great interest to OCaml developers. For those who have been exploring Dune’s experimental package management capabilities over the past six months, you’ll be pleased to know that we've recently merged a feature allowing OCaml compiler packages to be installed directly through Dune.

+

Until now, Dune’s Package Management has supported the installation of various packages from the opam repository. However, it lacked the ability to install a functioning OCaml compiler — a crucial component for most Dune projects. This limitation meant that early adopters of Dune’s Package Management had to rely on external tools to manage their OCaml compiler installations, which wasn’t ideal. The good news is that this obstacle has been removed, making Dune Package Management far more robust and ready for testing by early adopters.

+

The challenge we faced in integrating the OCaml compiler installation stemmed from a conflict between the compiler’s build system and the way Dune handles package builds. Dune builds packages in what’s known as a “sandbox” — a temporary directory where a package is initially constructed and installed. Once the build is complete, the package's installed components are moved to their final destination within Dune’s build directory. However, the OCaml compiler assumes that its installation location will be its permanent home. Moving the installed files after installation caused the compiler to malfunction, making this an intractable problem for Dune’s package management.

+

While work is underway to make the OCaml compiler more flexible in terms of its installation location, we didn’t want to delay Dune’s package management features until this work was completed. Instead, we’ve introduced a workaround that allows compiler packages to be installed in a way that maintains their functionality.

+

The solution involves installing OCaml compiler packages to a global, per-user directory, rather than within the project’s sandbox. By default, the compiler is installed in a directory such as ~/.cache/dune/toolchains/ocaml-base-compiler.<version>-<hash>. This ensures that the compiler remains in its expected location and operates correctly without the need for relocation.

+

Moreover, this approach offers an added benefit: compilers installed through Dune can be shared across multiple projects. If two projects use the same version of the compiler, the installation step can be skipped in the second project, significantly speeding up the build process. Given that installing an OCaml compiler can take several minutes, this optimisation will save developers considerable time.

+

In summary, this new feature represents a substantial improvement to Dune’s Package Management system, making it easier and faster for developers to set up and manage their OCaml projects. By enabling direct installation of OCaml compilers through Dune, we’re removing a major barrier to adoption and enhancing the overall development experience.

+

Since it works transparently whenever you build a project with the Developer Preview, we'd love for you to test it out! Try out the new Dune Developer Preview today, and let us know how it goes on Discuss. We’re eager to see how the community leverages this new capability and look forward to your feedback as we continue to refine and expand Dune’s Package Management features.

+ diff --git a/data/planet/tarides/dune-package-management-revolutionising-ocaml-development.md b/data/planet/tarides/dune-package-management-revolutionising-ocaml-development.md new file mode 100644 index 0000000000..609bad5668 --- /dev/null +++ b/data/planet/tarides/dune-package-management-revolutionising-ocaml-development.md @@ -0,0 +1,32 @@ +--- +title: 'Dune Package Management: Revolutionising OCaml Development' +description: Dune Package Management MVP completed in Q1 2024, unifying OCaml workflows. + Enabled complex project builds with new features, enhancing development experience. +url: https://tarides.com/blog/2024-10-09-dune-package-management-revolutionising-ocaml-development +date: 2024-10-09T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/DPM-1360w.webp +authors: +- Tarides +source: +--- + +

At Tarides, we’ve been working on an initiative to improve the OCaml development experience: Dune Package Management. As outlined in the Platform Roadmap, which was created through community collaboration, the aim is to unify all OCaml development workflows under a single, streamlined tool. At Tarides, we aim to make Dune the recommended frontend for the OCaml Platform, offering new users a seamless developer experience.

+

The motivation behind Dune Package Management is clear. For years, the OCaml community has called for a single tool to address all the development concerns: building projects, managing dependencies, testing on different compiler versions, etc. By integrating package management directly into Dune, we want to resolve the above long-standing pain points that can make OCaml cumbersome to work with, both for newcomers and experienced developers.

+

The Vision for Dune

+

Our long-term goal is to make Dune the central tool for OCaml development. That means more than just feature additions! It's about radically simplifying how developers work with the OCaml platform. By making installation painless and simplifying frustrating workflows, such as the handling of dependencies and testing against multiple compiler versions, Dune will address all your OCaml needs.

+

Dune integrates package management by using opam as a libary in essential parts of our approach. Two commands lie at the heart of integration: dune pkg lock and dune build. dune pkg lock creates a generated lock file, whereas dune build depends on this lock file to manage project dependencies. You can now handle everything from project initialisation to dependency management using these simple commands.

+

What We’ve Achieved So Far

+

We've accomplished a lot in these past few months! The work we have done for Dune Package Management can already handle such complex projects as OCaml.org and Bonsai using the new package management features. Both were successfully built using these new features. These early successes confirm our hypothesis: we are on the right track, because this proves the solution's viability in real world scenarios.

+

But this is not the end of the work. In the future, we plan to further improve the UX so that Dune is not only correct but also easy and productive for developers to use. The remaining challenges are yet to be overcome, and we hope to make Dune Package Management the standard tooling for all OCaml workflows.

+

The Road Ahead

+

Now that we hit the milestone for MVP, the subsequent phase will have testing, validation, and enhancement of the developer experience. Our main focuses going ahead will include:

+ +

A Unified Future for OCaml

+

Package Management brings in a new era of OCaml development. Dune will now be the only tool engineers will need, making OCaml development as seamless and effective for both complete beginners and experienced developers on the platform.

+

We look forward to the future and what Dune Package Management will facilitate within the OCaml community. Stay tuned, and prepare to take part in a more integrated and seamless OCaml development experience with Dune.

+ diff --git a/data/planet/tarides/easy-debugging-for-ocaml-with-lldb.md b/data/planet/tarides/easy-debugging-for-ocaml-with-lldb.md new file mode 100644 index 0000000000..d07f935486 --- /dev/null +++ b/data/planet/tarides/easy-debugging-for-ocaml-with-lldb.md @@ -0,0 +1,23 @@ +--- +title: Easy Debugging for OCaml With LLDB +description: Explore debugging OCaml programs using LLDB on macOS, as detailed by + Tim McGilchrist. Learn practical tips for handling OCaml's optimized code and more. +url: https://tarides.com/blog/2024-09-05-easy-debugging-for-ocaml-with-lldb +date: 2024-09-05T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/lldb_debug-1360w.webp +authors: +- Tarides +source: +--- + +

If you’re just getting started with OCaml, you may be wondering how to effectively debug your code when things go wrong. Fortunately, OCaml's ecosystem has evolved, offering modern tools that make debugging a more approachable task.

+

Tarides engineer Tim McGilchrist recently wrote a blog post that explores how to debug OCaml programs using LLDB on macOS. Developers familiar with languages like C, C++, or Rust may already have experience using LLDB, as it is a common choice on Linux or FreeBSD. LLDB is also the debugger that ships with XCode on macOS.

+

The Role of LLDB in OCaml Debugging

+

OCaml has traditionally used its built-in debugging tool ocamldebug for OCaml bytecode, but LLDB offers a way to debug native executables.

+

LLDB, the debugger from the LLVM project, offers a powerful way to inspect and debug compiled programs. While LLDB is not specific to OCaml, Tim's blog post highlights how it can be effectively used to debug OCaml code.

+

Tips and Tricks

+

Tim's post also provides practical tips for getting the most out of LLDB when working with OCaml. For instance, it discusses how to deal with OCaml’s optimised code, which can sometimes make debugging more challenging. It suggests compiling without certain optimisations when debugging complex issues, to ensure that the debugging information remains intact and the code paths are easier to follow.

+

Final Thoughts

+

Debugging is a critical skill for any developer, and mastering it in OCaml can significantly improve your productivity and code quality. The method outlined in Tim's post demystifies the process of using LLDB with OCaml, making it more accessible to those who are new to the language or who may be transitioning from other programming environments.

+

If you’re eager to dive deeper, please read Tim's full blog post, which gives both detailed instructions and examples to help you get started. With these tools at your disposal, debugging OCaml code becomes a much more manageable task. Happy coding!

+ diff --git a/data/planet/tarides/eio-from-a-users-perspective-an-interview-with-simon-grondin.md b/data/planet/tarides/eio-from-a-users-perspective-an-interview-with-simon-grondin.md new file mode 100644 index 0000000000..b37c2f4a67 --- /dev/null +++ b/data/planet/tarides/eio-from-a-users-perspective-an-interview-with-simon-grondin.md @@ -0,0 +1,52 @@ +--- +title: 'Eio From a User''s Perspective: An Interview With Simon Grondin' +description: Discover how the Eio library was enhanced with Simon Grondin's contributions, + addressing concurrency challenges and improving performance for OCaml projects. +url: https://tarides.com/blog/2024-09-19-eio-from-a-user-s-perspective-an-interview-with-simon-grondin +date: 2024-09-19T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/juggling-eio-1360w.webp +authors: +- Tarides +source: +--- + +

Are you curious about Eio but not sure what to expect? Eio is an effects-based direct-style concurrency library for OCaml 5. I recently spoke with Simon Grondin from Asemio about his personal experience using the I/O library Eio. He was kind enough to share the good and the bad and give me insight into how the library has worked for his projects.

+

If you want to know what programming with Eio is like from another user's perspective, this interview is for you. Let's explore what Simon had to say!

+

The Interview

+

"Hello Simon, thank you for meeting with me today! What first got you curious about Eio?"

+

“We use OCaml at Asemio, and I use OCaml a lot for my own projects. But when it came to concurrent code, I had accepted that to reap the benefits, I needed to deal with the increased complexity that came with them. In traditional concurrency, the developer relies on abstractions for tasks and promises using async/await. I had grown to assume that coloured functions was a necessary price to pay when the Eio library with its effect handlers announced that we didn't have to deal with this problem at all."

+
+

"Concurrency squeezes more out of code, so people use it, accepting that they will pay the cost of increased complexity. But we can enjoy the benefits of concurrency without the cost!"

+
+

"I had heard of Eio relatively early in its development, around version 0.3. At that point, it was still in flux, and I wasn't comfortable that I could build something lasting on top. Then I saw the announcement post for version 0.10 on June 11th 2023, and that's when I decided to try and switch. The project looked much more stable, the developers had resolved several initial issues, and the code wasn't being rewritten nearly as much as before. All of my previous hesitations had been addressed.”

+

"What did you do next?"

+

“I had a project in mind for testing Eio, a tool I had initially developed as an internal application. At Asemio, we regularly process huge Excel files (think millions of cells). The challenge with these files is that there are multiple ways that they can be organised internally, and it is impossible to know how they are organised without opening them. We need to be able to stream and read the data of very large files.

+

This is where the SZXX library comes in. It's a streaming ZIP, XML, and XLSX library that can stream data from these file formats even when reading from a network socket, either in constant memory or with user-defined memory usage guarantees. I had initially used the Lwt library to implement concurrency in SZXX, but I decided to convert it to Eio.”

+

"What benefit did you expect to see from switching to Eio?"

+

“From my perspective, the main problem with using Lwt was the function colouring problem. Micromanaging code in that way is time-consuming, and I wanted to learn Eio mainly because I knew that effects could potentially eliminate the extra work and complexity that came with Lwt.

+

I also learned that Eio came with integrated access to io_uring, letting the developer use it without additional effort and the function colouring problem. These were the two features I was the most interested in when converting the SZXX project from Lwt to Eio.

+

In addition, I had observed a split between Lwt and Async within the community, and for a while, I had been looking for a solution that could bridge the gap. From my research into the I/O library at that time, I felt confident that it had the potential to 'heal the split' between the different library users. In a way, converting SZXX to Eio was my way of testing that theory to see what effect the transition would have."

+

"What was your initial experience with Eio? Did you have any frustrations?"

+

"I actually did! When I first started using Eio, I had a hard time understanding how Paths, Flows, Files (and others) relate to one another. I also experienced a lack of documentation and examples of abstraction to help the newcomer get up and running. These are some of the first things a new user will experiment with, and they must work well. Since then, I have helped improve the documentation (alongside several other contributors) and made other quality-of-life contributions to the library."

+

These initial friction points were not enough to dissuade me from continuing my project, and after that initial hurdle, I was very happy."

+
+

"I had been prepared to accept a performance degradation to get the benefits I was looking for, but I was pleasantly surprised to note that performance actually improved.”

+
+

"That's great! Did Eio affect your project in any other ways? Did anything surprise you?"

+

“I was unprepared for just how much of a difference using non-monadic code would make. Eio has this concept called a Switch, which ties resources to scopes. It cleans up your code by managing the lifecycle of open resources automatically, for example, turning off background processes, closing file handles, and ensuring that all auxiliary states are set to their desired state upon exiting the scope.

+

When you write parallel programs, there can be hundreds of thousands of interleavings and computations, and ensuring that each computation is handled correctly has always been a challenge with monadic-style code. But with Eio and effects-based concurrency, the switch handles much of that complexity for you.

+

In fact, both of these benefits work synergistically. They include solving the function colouring problem (meaning you don't need to distinguish between async and 'normal' functions) and using non-monadic code. Each amplifies the other almost exponentially and frees up a lot of your complexity budget."

+
+

"The human brain limits the complexity of code, and at some point, you just can't keep making things smaller to make them simple enough. Eio helps reduce complexity. With Eio, I was able to simplify and remove so much bloat from the code and achieve some really tricky optimisations, pushing the limit of what was possible.”

+
+

"That's an interesting insight, and I think one that only someone with real user experience can make. It's great to hear what results the user might expect. I know you have made significant contributions to Eio as well, and that the team has made you a maintainer in response to your contributions and reviews. Can you tell me about some of those?"

+

“I started contributing to Eio from around version 0.11 and onwards. Some of my main projects include: executor_pool, developing an Eio adapter for the popular CSV library that I also added to Angstrom, as well as work on an internal thread pool to speed up platforms without io_uring support. Along the way, I have added resources to Eio that make it easier for people to adopt the tool. For example, I designed the executor_pool module based on common patterns that I had often used in my projects.

+

Regarding the adaptors, in OCaml, library authors need to explicitly write one adaptor per I/O library they choose to support. The popular CSV library already had adaptors for both Async and Lwt. I knew that it would be hard for certain users to pick up Eio if it did not have an adaptor, so I wrote one and added it to both CSV and Angstrom. A lot of OCaml software depends on Angstrom through one dependency or another, and without Eio support, those codebases cannot make the switch to Eio.”

+

"Thank you for answering my questions and sharing your experience with Eio! Do you have any final thoughts you would like to share?"

+
+

“Eio helped me reason about my code, and I discovered bugs and problems because of how much Eio had cleaned up the code. I uncovered hidden bugs in every program I converted from Lwt to Eio. Every single one also ended up being faster, not because Eio itself was faster (it was as fast as Lwt), but because of the optimisations I could now afford to make, thanks to the reduced complexity.”

+
+

Stay in Touch

+

If you have questions about Eio or how to use it, you can fill in our contact form, and we will contact you. You can also ask questions on the OCaml Discuss forum or open issues and pull requests in the Eio repo.

+

To keep up with our activities, you can always follow us on X (formerly known as Twitter), LinkedIn, Mastodon, Threads. We look forward to connecting with you!

+ diff --git a/data/planet/tarides/feature-parity-series-compaction-is-back.md b/data/planet/tarides/feature-parity-series-compaction-is-back.md new file mode 100644 index 0000000000..ca7bf5ee5d --- /dev/null +++ b/data/planet/tarides/feature-parity-series-compaction-is-back.md @@ -0,0 +1,59 @@ +--- +title: 'Feature Parity Series: Compaction is Back!' +description: Achieved compaction compatibility for OCaml 5.2, restoring a key feature + to the garbage collector for enhanced memory management in multicore environments. +url: https://tarides.com/blog/2024-09-11-feature-parity-series-compaction-is-back +date: 2024-09-11T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/truckcompaction-1360w.webp +authors: +- Tarides +source: +--- + +

Compaction is a feature that rearranges OCaml values in memory to free up space, which can then be returned to the operating system. In the OCaml 5.2 release, the technique returns to the OCaml Garbage Collector for the first time since its removal in the 5.0 multicore update.

+

This is part one of our feature parity series highlighting features returning to OCaml in an effort to restore feature parity with OCaml 4.14. When OCaml gained multicore support (that is, the ability to execute on multiple domains) it had far-reaching implications on the way the runtime worked, and as a result, support for some features were dropped for the 5.0 release. To address these gaps, a significant amount of work has been done behind the scenes to adapt tools and runtime features to work safely and performantly with multiple domains. Tarides is part of the effort to restore these familiar features to OCaml 5.

+

What is Compaction?

+

In OCaml 5.0, the major heap in the parallel Garbage Collector employs size-segregated pools attached to each domain. Over time, as OCaml domains allocate and discard heap values, many of these pools end up being only partially used. For example, a program might allocate millions of two-element tuples when initialising but no longer need most of these afterwards. This will result in lots of 'size two' pools, most of which will only be sparsely filled. This is inefficient as OCaml will still consume system memory for all the pools, even if the heap values only take up a tiny proportion of each pool.

+

Compaction is not new to OCaml; the latest version to include the technique was 4.14. After OCaml adopted a multicore garbage collector, compaction needed to be rewritten to work with the major heap's new structure and to be safe in parallel execution. Compaction for OCaml 5 - as reintroduced in PR #12193 - achieved this by identifying a small number of shared pools in each size class big enough to contain all heap values in that size and then moving all heap values in the remaining pools into the selected pools. This results in many empty pools, the memory of which can be returned to the operating system.

+

The new algorithm is entirely different from the previous one, so let's look at how it works!

+

Compaction in 5.2

+

Allocating Into the Major Heap

+

Simply put, compaction is a means of rearranging fragmented pieces of memory to larger - compact - chunks. To understand how the compaction introduced in 5.2 works, we must first understand how allocation works in the GC's major heap (you may want to skip this part if you're already familiar with the process). When you first allocate a value in the major heap, it is given a size from a size class table. Each size class, in turn, lists four different ways a pool can be stored: unswept available, unswept full, available, and full.

+

These pools are divided into blocks, and each pool contains a number of blocks of the same size class. When we allocate a value, an appropriate size class is chosen depending on the size of the value, and the first pool with space available in that class is selected. The header of that pool has a pointer indicating the next available block, and the value is written into that memory block. Each domain is responsible for this process independent of other domains. This is crucial for acceptable performance in parallel programming.

+

When the GC sweeps the pools, it will free certain blocks and add them to the free list in the header of their pool. After a while, cycles of sweeping and allocation create pools with free ('empty') blocks interspersed among live ('full') blocks. This process results in inefficient memory use and many partially filled pools.

+

Compacting the Major Heap

+

To address this inefficiency, the developer can compact the major heap and move the live blocks into an optimised order among the pools. In OCaml 5, this technique follows a specific sequence, which is as follows:

+

1. Barrier:
+Because this is parallel compaction, we must synchronise all the domains before proceeding. Each domain has its own heap, and the heaps are compacted in parallel, with each domain responsible for its own compaction. Synchronisation is achieved with the help of a barrier.

+

2. Size Class:
+The compaction process iterates through each size class, processing one at a time, starting with the smallest. A stats table is allocated for each domain, with a slot available for each pool of the current size class being processed. Since the GC has already swept everything we will be compacting, there are only two states a pool can be in, full or available, where the latter means there is free space available in it.

+

The process then continues by using the stats table to check whether pools are full or available (meaning they have at least one free block). This process means we don't delve deeply into the memory to read from it, and there is no cache contamination. There is no synchronisation between domains in this step, and the compaction process for a domain only proceeds from here if there is at least one available pool.

+

3. Using the Stats Table:
+By this time, each domain to be compacted will have a stats table with a list of all the available pools. In the next step, the process goes down each pool on the available list and counts the number of live and free blocks. This is done linearly through the pool.

+

Once the number of live and free blocks is known, the number of live blocks is deducted from the number of free blocks. The resulting number of free blocks lets us calculate which pools can be emptied and which will be retained. This is all the information we need from the stats table, so once this step is completed, the stats table is cleared.

+

4. Pool Pointers and Live Links:
+To summarise, we now know how much live space there is within the pools and how much free space we can liberate if we compact the live blocks together. To achieve compaction, we create pointers to two pools, one to the first pool we are evacuating and one to the first pool we are retaining (for those who are curious, these pointers are named current_pool and to_pool respectively).

+

The process starts with the first pool we know will be evacuated. It finds the first live block within that pool and uses the current_pool pointer to remove it from the pool and the to_pool pointer to insert it into one of the pools we know will still be live post-compaction (this information comes from the calculation we did using the stats table).

+

5. Compaction!:
+This is the operative part of compaction: copying all the live blocks from pools that will be evacuated into pools that will remain live after compaction using the two pointers. As this is done, the process writes forward pointers that point from the block where something used to be stored forward to the block where it is now stored post-compaction.

+

6. Barrier 2:
+Again, another barrier syncs all the domains – a crucial part of compaction on multiple domains.

+

7. Scanning:
+This part of compaction is the most expensive in terms of time. The entire OCaml heap has to be scanned for pointers pointing to old block locations (moved as the pool they were in was evacuated), and old pointers must be updated using the forward pointers. Each domain is responsible for updating its data.

+

This is a deceptively extensive process. For example, even pointers in objects that are too large for the size allocator (so over 128 words) and therefore never moved by compaction may still need to be updated after the compaction process as they may also contain pointers to the old block locations.

+

8. Barrier 3:
+Another barrier synchronises between domains.

+

10. Freeing Evacuated Pools:
+All the evacuated pools are freed and added to the free list.

+

11. Barrier 4:
+Another barrier to synchronise between domains.

+

12. Release Memory:
+One domain, whichever is the first one to get to that point, unmaps the free list. This means that the memory we asked the OS for initially, which currently belongs to the OCaml system, is released at this point and goes back to the OS. This is the end benefit of compaction; it reduces the size of the OCaml system on your machine and returns memory to the OS for use elsewhere.

+

Final Details & Next Steps

+

Before we wrap up, let's look at one more detail about how compaction works in 5.2. In 5.2, compaction uses a slab allocator and size classes, whereas OCaml 4 uses a free list. This means that OCaml 5.2 does not provide the option to set an allocation policy like OCaml 4.14. Our testing has found that for most workloads, the chosen allocation policy (using the size classes) performs well. However, expert users can tune the configuration of the size classes in gen_sizeclasses.ml (necessitating that they build their own OCaml), which they may find useful for their own projects. This is just one example of the challenge that comes with adapting a feature as complex as compaction to be compatible with multiple cores, and the careful weighing of pros and cons it requires on behalf of the developers.

+

The next steps for OCaml 5 are the expected restoration of MSVC backends, Statmemprof support, and the return of the unloadable runtime coming in releases 5.3 and 5.4. Keep a look out for future posts detailing those features and the efforts put toward bringing them back.

+

It's great to have compaction restored to OCaml, and it is a testament to the hard work of several teams within Tarides and the wider open-source community surrounding OCaml. We are happy to be part of the team working on this secure and performant programming language.

+

Share Your Experience!

+

We want to understand your experience! We're open to suggestions and feedback about the process to help us optimise the feature and deal with any pain points. You can share your thoughts on OCaml's discussion forum or make suggestions directly in the repo.

+

You can stay in touch with us on X, Mastodon, Threads, and LinkedIn. We look forward to hearing from you!

+ diff --git a/data/planet/tarides/getting-specific-announcing-the-gospel-and-ortac-projects.md b/data/planet/tarides/getting-specific-announcing-the-gospel-and-ortac-projects.md new file mode 100644 index 0000000000..25fa12ea4b --- /dev/null +++ b/data/planet/tarides/getting-specific-announcing-the-gospel-and-ortac-projects.md @@ -0,0 +1,54 @@ +--- +title: 'Getting Specific: Announcing the Gospel and Ortac Projects' +description: Developed Gospel and Ortac, enhancing OCaml's specification language + and runtime assertion checking tools, through collaboration with ANR, INRIA, and + others. +url: https://tarides.com/blog/2024-09-03-getting-specific-announcing-the-gospel-and-ortac-projects +date: 2024-09-03T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/magnifying-glass-1360w.webp +authors: +- Tarides +source: +--- + +

Part of the benefit of open-source development is the opportunity to collaborate on projects across traditional organisational boundaries, such as academia and industry. Tarides is part of a larger effort to develop a behavioural specification language and associated tooling for OCaml. The project creates an easy-to-use foundation for formal specifications, allowing users to include them in generated documentation and perform automated testing and verification. This important work is funded in part by ANR.

+

The Gospel Project

+

The French National Research Agency (ANR) is a public institution in France that funds innovative research projects where public institutions collaborate with each other or the private sector. OCaml was invented at the French National Institute for Research in Digital Science and Technology, INRIA, and ANR is funding a research project as a collaboration between INRIA, Tarides, LMF UPSaclay, and Nomadic Labs. The goal of the project is to develop and improve the specification language Gospel alongside its tooling ecosystem and demonstrate its usefulness in different case studies.

+

What is Gospel?

+

Gospel is a contract-based behavioural specification language that allows you to write specifications in the module interface you want to specify. As a specification language, it is a formal language, meaning its semantics are precisely defined (by means of translation into Separation Logic, see this paper).

+

By behavioural specification language, we mean a language that allows you to describe the expected functional behaviour of a function. Specifications don't reference resources such as CPU time or memory size, but only what the program does (so-called functional behaviour). Expected behaviour is expressed as a contract. The basic premise is that as long as the user of the library calls functions with arguments that respect the expressed preconditions, then the implementation of the library should behave per their description.

+

Per se, Gospel doesn't guarantee that your implementation respects its given specifications, it is simply a language that allows you to express precisely what your code should do. However, note that Gospel still comes with a type-checker. This type-checker lets you check that your specifications are well-formed and in sync with the interface. For example, if you add an extra argument to a function in your library, the Gospel type-checker will tell you if you forgot to update the specifications accordingly.

+

Gospel is a relatively new specification language and is bound to evolve, but it is already mature enough to specify a diverse set of libraries. It provides developers with a non-invasive and easy-to-use syntax to annotate their module interfaces with formal contracts describing type invariants, mutability, function pre- and postconditions, exceptions, etc. +For example, let's say you want to specify a fixed-size stack. The type declaration in the module interface would look like:

+
type a t
+(*@ model capacity : integer
+    mutable model contents : a sequence
+    with s
+    invariant Sequence.length s.contents <= s.capacity *)
+
+

You give two logical models to your datatype: an immutable one for the capacity of the stack and a mutable one for the content. Then, given a stack, s, you can formulate type invariants. Namely, the stack should not have more elements than capacity allows. +The specification for the create function would look like:

+
val create : int -> 'a t
+(*@ s = create n
+    requires n > 0
+    ensures s.capacity = n
+    ensures s.contents = Sequence.empty *)
+
+

The first line binds the arguments and the returned value to names so that we can talk about them. Then we express the precondition that the given argument should be strictly positive and the two postconditions that fill the logical models as expected.

+

Gospel is also a tool-agnostic specification language, meaning it doesn’t make any assumption about how and by which tools its specifications will be consumed. Some users use Gospel specifications to provide proofs of functional correctness for their implementations. For example, Cameleer does so by leveraging the power of the Why3 deductive verification platform. At Tarides, with the Ortac project, we explore how to use Gospel specifications to do runtime assertion checking.

+

Gospel was initially developed by Cláudio Lourenço (LRI post-doctorate) and is currently maintained by Jean-Christophe Filliâtre, Samuel Hym, Nicolas Osborne, and Mário Pereira. Clément Pascutto also maintained Gospel for several years as part of his PhD work at Tarides and LRI.

+

A Tool for Gospel: Ortac

+

Ortac stands for OCaml RunTime Assertion Checking. Clément's PhD thesis initiated the Ortac project which has since grown into a greater cooperative effort. Samuel Hym and Nicolas Osborne currently maintain it. At its core, Ortac translates the computable subset of Gospel terms into OCaml code. In addition, it provides a plugin architecture to implement different uses of this translation. Translating Gospel terms into runnable OCaml code opens the possibility of checking an implementation against the interface specification at runtime.

+

Three plugins have been built upon this translation, plus a fourth one, which is slightly different. Let’s take a look:

+
    +
  1. The Ortac/Wrapper plugin was developed during Clément's PhD. Given the Gospel specified interface of a module, this plugin generates a new module with the same interface, wrapping the initial implementation with runtime checks coming from Gospel specifications. When a Gospel specification is violated by the client for preconditions or by the initial implementation for postconditions, the wrapped version will output an error message providing the user with useful information, such as which Gospel clause they have violated. Users can then use the new wrapped module in place of the original one in their project, to, for example, aid in debugging efforts. This plugin is still considered experimental.
    2. +
  2. The Ortac/Monolith plugin, which is based on Ortac/Wrapper and is the product of an internship, was presented at ICFP 2021. Given the specified interface of a module, this plugin generates the Monolith standalone program, testing the initial implementation against the wrapped one. The idea is that, in case the implementation doesn't respect the specification, the wrapped version will return a special Ortac error while the bare initial one won't. Monolith allows you to use fuzzing to test your library and provides a runnable scenario that demonstrates the unexpected behaviour. This plugin is also still considered experimental.
    3. +
  3. The Ortac/QCheck-STM plugin is based on Naomi Spargo's internship project. Given the specified interface of a module and some user-provided extra information, this plugin generates standalone QCheck-STM tests. In addition to avoiding having to write the QCheck-STM test by hand and as a recently added feature, in case of a test failure, the generated tests will inform you which part of the specification has been violated, give you a runnable scenario demonstrating the unexpected behaviour, and the expected returned value when the Gospel specifications allow to compute it. This plugin has been released.
    4. +
  4. The Ortac/Dune plugin is slightly different as it doesn't rely on a Gospel specification. Instead, it helps you by generating the Dune rules necessary to run another plugin. So far, only the command for Dune rules related to the Ortac/QCheck-STM plugin is available, as it is the only one that has been released. The command yields the Dune rules required to generate and run the tests.
    5. +
+

Future Steps

+

Regarding Ortac, the 0.3.0 version of a set of Ortac packages, including the first Ortac/Dune release, has recently been published. Among other improvements and fixes, this release makes dynamic formal verification with Ortac very easy. The team is now investigating how to test more functions by lifting some limitations that come with a naive use of the QCheck-STM test framework, with an intern (Nikolaus Huber) working on this last topic.

+

With Gospel 0.3.0 published, the upcoming goals centre around continuing maintenance and development, using our engineering expertise to help our research partners bring new features to the Gospel language.

+

Until Next Time

+

Do you want to try out Gospel and Ortac? Check out the documentation and report back on your experience! If you want to stay informed about our projects, follow us on X (formerly known as Twitter) and LinkedIn for all our latest updates. Are you interested in using Gospel for your own projects? Contact us, and we will be happy to discuss the benefits of implementing specification languages in your workflow.

+ diff --git a/data/planet/tarides/how-tsan-makes-ocaml-better-data-races-caught-and-fixed.md b/data/planet/tarides/how-tsan-makes-ocaml-better-data-races-caught-and-fixed.md new file mode 100644 index 0000000000..a1169a539a --- /dev/null +++ b/data/planet/tarides/how-tsan-makes-ocaml-better-data-races-caught-and-fixed.md @@ -0,0 +1,46 @@ +--- +title: 'How TSan Makes OCaml Better: Data Races Caught and Fixed' +description: Explore how TSan caught data races in OCaml, leading to bug fixes in + the 5.2 update, enhancing memory safety and performance with improved runtime operations. +url: https://tarides.com/blog/2024-08-21-how-tsan-makes-ocaml-better-data-races-caught-and-fixed +date: 2024-08-21T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/toolswall-1360w.webp +authors: +- Tarides +source: +--- + +

Parallel programming opens up brand-new possibilities. Using multiple cores means that users can benefit from powerful OCaml features (like formal proofs and high security) while enjoying greater performance, enabling them to improve their services or projects.

+

However, introducing such a significant change to the OCaml ecosystem would not be practical without providing tools that help users ensure memory safety in parallel programming. This is where multicore tests come in, as does ThreadSanitizer (TSan) support for OCaml. We have published two previous posts on TSan, an overview of the tool and an introduction to the danger of data races in general. This post will give you a behind-the-scenes look at how we have used TSan to find and fix races in the OCaml runtime. Official support for TSan arrived with OCaml 5.2, but as you can tell from the repository, we have been using TSan internally for a while now.

+

Catching Races in OCaml

+

As a result of TSan coming with the OCaml 5.2 update, several bug fixes in the same update addressed data races. A data race occurs when two accesses are made to the same memory location; at least one is a write, and no order is enforced between them. Data race bugs can be hard to spot, but since they can result in unexpected behaviours, they are a high-priority item to fix.

+

It is important to note that not all data races are equal. In OCaml, the memory model guarantees that memory safety is preserved even when data races occur. This makes data races in OCaml much 'safer' than in many other languages, where races can impact memory safety. OCaml programs also require support from the OCaml runtime which provides low-level operations such as memory allocation and garbage collection. The OCaml runtime is written in C and must be data race-free according to the C memory model since a data race in the runtime would impact the validity of the whole program. While TSan has been integrated to detect data races in OCaml code, it has also proven invaluable in detecting errors in OCaml's runtime, many of which were subsequently fixed in 5.2.

+

What has TSan Caught so Far?

+

Ecosystem contributors make continuous efforts towards maintenance, and as part of this work, use TSan to check the OCaml runtime. To further simplify TSan usage we have added a TSan Continuous Integration (CI) run that executes the OCaml test suite in a TSan-enabled switch, automatically detecting inadvertently introduced data races in the runtime. This has allowed us to catch and fix several data races. +Some of these include:

+ +

Until Next Time!

+

Seeing a tool we have developed so quickly benefit the larger ecosystem is excellent. TSan helps developers test their parallel programs for potential risks they would have difficulty discovering. We look forward to seeing users put TSan to the test and share the results!

+

The OCaml community welcomes contributions and feedback and invites users to share any issues in the OCaml GitHub repo. The discussion forum OCaml Discuss is another place to share your thoughts and get input from others in the community.

+

Would you like to stay up-to-date with us? Follow us on X (formerly known as Twitter) and LinkedIn to see regular posts on our projects, announcements, tutorials, and more.

+ diff --git a/data/planet/tarides/introducing-dune-the-essential-build-system-for-ocaml-developers.md b/data/planet/tarides/introducing-dune-the-essential-build-system-for-ocaml-developers.md new file mode 100644 index 0000000000..da764734f0 --- /dev/null +++ b/data/planet/tarides/introducing-dune-the-essential-build-system-for-ocaml-developers.md @@ -0,0 +1,39 @@ +--- +title: 'Introducing Dune: The Essential Build System for OCaml Developers' +description: Exploring Dune as OCaml's official build system, providing automated + compilation, dependency management, and a robust foundation for efficient code development. +url: https://tarides.com/blog/2024-09-26-introducing-dune-the-essential-build-system-for-ocaml-developers +date: 2024-09-26T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/intro_dune-1360w.webp +authors: +- Tarides +source: +--- + +

One of the first tools you'll encounter when adopting OCaml is Dune, OCaml's official build system. Understanding what Dune is and how it serves you is key to crafting everything from a small project to maintaining large-scale codebases. So let's dive in! Learn how Dune makes development easier and serves as a gateway to the greater OCaml Platform.

+

For a quick introduction to OCaml, check out the tutorials on OCaml.org.

+

What is Dune?

+

Dune is much more than a simple build tool. It automatically compiles your OCaml code, manages its dependencies, and generates the final executable or library. It's also a well-maintained, highly-optimised platform that streamlines your development process. Spend more time writing code and less on struggling with complex build rules.

+

Advantages of Dune

+

1. Consistency Across Projects

+

With Dune, you can be sure that the build processes are consistent, no matter how many different projects you are managing. This is very helpful when collaborating with other developers or when maintaining multiple projects. Once you work with Dune on one project, it's easier to work on the next, even if it has a totally different codebase, because Dune standardises how things are done.

+

2. Integration With the OCaml Platform

+

Dune lives on the cutting edge of the OCaml Platform (a set of tools and libraries) and forms a solid foundation for your development environment. Dune automatically plays nicely with other tools such as opam (an OCaml package manager) and helps you manage dependencies, run tests, and set up project documentation.

+

3. Performance Optimisation

+

Dune is fast and efficient. It tracks dependencies and rebuilds only when necessary, so your development processes will be more responsive. This performance optimisation benefits the developer, regardless of project size. Although for big projects, it especially makes a difference because it significantly reduces the build time.

+

Dune also supports other languages and tools within the same project. This flexibility makes it easy to incorporate C stubs, inline assembly, or even JavaScript (via js_of_ocaml and Melange) into your OCaml projects without needing to change your build system.

+

A Well-Maintained and Evolving Tool

+

The Dune team listens to community needs and regularly releases updates for performance, features, and bug fixes. This keeps Dune current with OCaml's development, giving engineers a coherent and state-of-the-art tool that evolves with the language and ecosystem.

+

Soon, Dune will also provide package managing functionality, so you can choose whether to use Dune or opam. It's currently in beta testing, so watch this blog for an announcement of the upcoming release!

+

Getting Started With Dune

+

It is very easy to install Dune using opam:

+
opam install dune
+
+

Now make a new OCaml project by running:

+
dune init project my_project
+
+

This creates a minimal project structure with sensible defaults, so you can get to coding right away. When ready, compile your project using dune build and run it using dune exec ./my_project.

+

Conclusion

+

Dune simplifies the development process, ensures uniformity, and is deeply integrated with the entire OCaml Platform. If you set up Dune from the very beginning, it will let you focus on creating great software, the most important thing.

+

As you learn more about OCaml, you'll appreciate the power, flexibility, and great community behind Dune and OCaml as a whole. For both small personal projects and collaborations on big applications, Dune is a tool you can rely on from start to finish.

+ diff --git a/data/planet/tarides/introducing-olly-providing-observability-tools-for-ocaml-5.md b/data/planet/tarides/introducing-olly-providing-observability-tools-for-ocaml-5.md new file mode 100644 index 0000000000..cbd8173c61 --- /dev/null +++ b/data/planet/tarides/introducing-olly-providing-observability-tools-for-ocaml-5.md @@ -0,0 +1,35 @@ +--- +title: 'Introducing Olly: Providing Observability Tools for OCaml 5' +description: Explore Olly, a powerful observability tool for OCaml 5, offering modular + features to visualize runtime data. Learn the latest enhancements and usage tips. +url: https://tarides.com/blog/2024-07-03-introducing-olly-providing-observability-tools-for-ocaml-5 +date: 2024-07-03T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/ollydata-1360w.webp +authors: +- Tarides +source: +--- + +

It might be tempting to think that we can write code that works perfectly the first time around, but in reality optimisation and troubleshooting forms a big part of programming. However, there are more and less productive (and frustrating!) ways of problem solving. Having the right tools to guide you, ones that show you where to look and what is going wrong, can make a huge difference.

+

We recently introduced you to the monitoring system runtime_events, which allows users to monitor their runtime for, among other things, how programs are affecting performance. Alongside runtime_events, sits the observability tool olly, which provides users with a number of helpful formatting options for their runtime tracing data.

+

This is all part of how we’re making developing in OCaml easier by bringing new features and tools to the community. Olly is just one such tool, and it makes the monitoring system for OCaml significantly more accessible. With Olly, you don’t have to be an expert or spend time combing through the data that runtime_events extracts for you. Rather, Olly can generate the information you need in a way that makes it easy to understand, store, and query.

+

What is Olly and How Does it Work?

+

Olly, as an observability tool for OCaml 5, has the ability to extract runtime tracing data from runtime_events. This data can then be visualised with a variety of graphical options available.

+

How does Olly do this? Olly uses the Runtime API to provide you with monitoring metric information and associated data. The tool comes with several subcommands, each with its own function.

+

The command olly trace can generate runtime traces for programs compiled in OCaml 5 using its trace subcommand. The tracing data is generated in one of two formats, the Fuschia trace format or the Chrome tracing format with the former being the default. Both formats can be viewed in Perfetto, but the Chrome format trace can also be viewed in chrome://tracing for Chromium-based browsers. Another example of a subcommand is olly gc-stats, which can report the running time of the garbage collector (GC) and the GC tail latency of an OCaml executable.

+

The motivation behind introducing an observability tool like Olly is to make data extracted using runtime_events more useful, since few developers will want to use the event tracing system directly. Olly makes it easy for users to troubleshoot their own programs, but it also makes it easy for a developer to diagnose why someone else’s program is slow. A client can send their runtime_events data, a feature that comes built in with every OCaml 5 switch, to a developer who can then use Olly to find the problem and suggest a solution. This makes working in OCaml is easier as optimisation and problem solving becomes more efficient and streamlined.

+

It doesn’t end there! One of our future goals for Olly is that it should be able to provide automatic reports and diagnosis of some problems. Look out for that exciting update in the future!

+

Recent Update: Modularising Olly

+

One of the latest updates to Olly is its modularisation by Eutro, splitting the bin/olly.ml file into smaller discrete libraries including olly_common, olly_trace, and olly_gc_stats. By splitting up the large file, the user can exercise some control over which dependencies they want their library to have. They can create a minimal build with minimal dependencies, or stick with a fuller build relying on all the dependencies. For example, to build olly_bare on the trunk you now only require two dependencies: Dune and cmdliner. Both can be installed without using Opam. Since some developers will prefer this set up, it’s good to support a variety of configurations.

+

It also potentially makes it easier to maintain, since the smaller files have well-defined purposes and provide a clearer overview than just having one large file covering a multitude of functions. If something breaks, this segmentation can make it easier for a maintainer to triage and amend the problem. The same modularisation may also help newcomers get an overview of all the different components of the library. Sadiq Jaffer merged Eutro’s PR #43 into Tarides: main and it will form part of a future Olly release pending further testing.

+

How to Use Olly: an Example

+

Let's wrap up by looking at an example of when you might use Olly. When we want to visualise the performance of the OCaml runtime alongside any custom events we may have, the first step is to generate a trace. To generate a trace, we run the command olly trace tracefile.trace in combination with the name of the program we want to enable tracing for. If we wanted to generate a trace for the solver-service, the command would be olly trace tracefile.trace 'solver-service'.

+

For our example, we chose to generate the tracing data in the Fuschia trace format. Once we had the trace, we loaded it into Perfetto to get a helpful visual representation of what our code is doing and we ended up with the following image:

+

A diagram representing different processes running left to right along the image in different colours: green, yellow, pink, and grey. The visual representations of the processes are stacked on top of one another, forming different bands.

+

The UI in this image displays the processes down the side, each corresponding to a domain. Our program ended up using four cores, and therefore, the image shows four processes. Each process, in turn, shows the tracing for the OCaml runtime build plus the custom events generated by Eio. Let's zoom in on one process now:

+

A diagram giving an expanded view of the events happening in process 0. The different activities are shown using various colours. Activities include ring_id 0 1, eio.exit_fiber:v:5, and eio_fiber:v:1

+

This expanded view shows both the Garbage Collector's (GC) activity and times when Eio is suspended.

+

Until Next Time!

+

We want to create tools that make the developer experience in OCaml easier and more intuitive. Olly makes it possible to visualise your code's performance, helping you understand when your programs are slowing down and why. If you have suggestions or improvements to share, you are welcome to participate in the Runtime Events Tools repo on GitHub.

+

We want to hear from you! Connect with us on social media by following us on X (formerly known as Twitter) and LinkedIn. You can also join in with the rest of the community on the forum Discuss to share your thoughts on everything OCaml!

+ diff --git a/data/planet/tarides/introducing-the-dune-developer-preview-a-new-era-for-ocaml-development.md b/data/planet/tarides/introducing-the-dune-developer-preview-a-new-era-for-ocaml-development.md new file mode 100644 index 0000000000..1b11f0d0e8 --- /dev/null +++ b/data/planet/tarides/introducing-the-dune-developer-preview-a-new-era-for-ocaml-development.md @@ -0,0 +1,34 @@ +--- +title: 'Introducing the Dune Developer Preview: A New Era for OCaml Development' +description: 'Discover Dune Developer Preview experimental release: new OCaml package + management and streamlined workflows, inspired by successful ecosystems like Rust.' +url: https://tarides.com/blog/2024-10-03-introducing-the-dune-developer-preview-a-new-era-for-ocaml-development +date: 2024-10-03T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/DDP-1360w.webp +authors: +- Tarides +source: +--- + +

The Dune team is excited to announce the arrival of Dune Developer Preview, an experimental nightly release of Dune created to test improvements, including the new package management feature. This is a major milestone for OCaml development! We've been working hard improving Dune, and we're excited to introduce this new way to ease OCaml workflows. If you are an OCaml developer, this is the time to explore the future of package management and development yourself.

+

Why the Wait?

+

Our progress has been slower than anticipated because the Dune project is a complex endeavour. We’re committed to balancing support for existing OCaml users while introducing new workflows. While opam remains the stable workflow and isn't going away, a key difference is that the Dune Developer Preview showcases experimental workflows. We believe, once fully ready, this will be transformative for the community. Meanwhile, we continue to maintain opam and its infrastructure, ensuring the OCaml ecosystem remains robust, with recent updates like opam 2.2 bringing proper Windows support.

+

Why the Change?

+

We have listened over time to your feedback and learned that while functional, the existing tooling around OCaml can be quite cumbersome. Our mission is to make OCaml development easier, faster and more enjoyable, and Dune is now about to become that all-in-one tool which does just that. This separation will allow Dune to cut down on the complexity and make its development process much lighter.

+

The Developer Preview gives a sneak peek into these improvements and provides an opportunity for developers to get their hands on these tools before the official release.

+

What's New in Dune?

+

The Dune Developer Preview introduces several major changes in how OCaml developers will work. Probably the most notable change is that it includes package management right within Dune itself. No more juggling with multiple tools; Dune does it all in one go.

+

Accordingly, the new Dune comes as a binary. That means it no longer requires the usage of opam to install it. You can simply just install Dune within minutes, and you'll be off to a flying start. That gives you so much more time for actual development.

+

Drawing Inspiration from the Best

+

Throughout this process, we've drawn inspiration from other successful ecosystems. We learned from Rust, Go, and Erlang the power of letting developers test and provide feedback on a pre-general release, and we are doing the same with Dune: giving the OCaml community a chance to have their say in shaping up the final form of this tool. Your input will be invaluable in refining Dune and ensuring it meets your needs.

+

Join the Beta

+

We are looking for developers to participate in the Dune Developer Preview. Experienced developers can help us put the latest features of Dune through their paces so that we can fine-tune the workflow to be smooth and intuitive across a range of projects. Those new to OCaml can test the workflow from their perspective of working in other ecosystems. Whether you have been using OCaml for years or are new to the OCaml ecosystem, your input is crucial in helping us make Dune the recommended tool for OCaml development.

+

To become a beta tester, one only needs to download the Dune Developer Preview. You will get the very latest version and immediately start playing with the new workflows and package management features. Your feedback will help to further shape the future of OCaml tooling, and we want to hear your thoughts on everything from usability to performance enhancements.

+

Measuring Success

+

Our goal is clear: use OCaml with as little ceremony as possible, so we set a few key benchmarks to make that happen. First: via Dune, the user should be able to fire up a new project in less than 10 seconds with no extra tooling required. This level of speed makes all the difference during everyday hacking.

+

We also monitor general developer satisfaction with the new Dune workflows. For the Net Promoter Score, we will know how likely a user is to recommend Dune to other users. Our objective is to reach +80, which shows great approval and satisfaction within the community.

+

What's Next?

+

This is only the beginning of the Dune Developer Preview. We will regularly update and enhance it based on feedback from beta testers. This includes polishing the new Dune Toolchain feature in order to automatically manage OCaml versions and development tools, and exploring new distribution channels in order for Dune to be even easier to download and use.

+

This is huge for OCaml, and we are excited to have you along for the ride. Why wait? Download the Dune Developer Preview today, and give some of the new workflows a try before letting us know what you think. With your help, we can make Dune the go-to tool for all OCaml development.

+

We can't wait to hear from you — and happy coding!

+ diff --git a/data/planet/tarides/introducing-the-odoc-cheatsheet-your-handy-guide-to-ocaml-documentation.md b/data/planet/tarides/introducing-the-odoc-cheatsheet-your-handy-guide-to-ocaml-documentation.md new file mode 100644 index 0000000000..4d5d58df2a --- /dev/null +++ b/data/planet/tarides/introducing-the-odoc-cheatsheet-your-handy-guide-to-ocaml-documentation.md @@ -0,0 +1,46 @@ +--- +title: 'Introducing the `odoc` Cheatsheet: Your Handy Guide to OCaml Documentation' +description: Discover the new `odoc` Cheatsheet, a concise guide simplifying OCaml + documentation generation with essential syntax and markup commands for efficient + coding. +url: https://tarides.com/blog/2024-09-17-introducing-the-odoc-cheatsheet-your-handy-guide-to-ocaml-documentation +date: 2024-09-17T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/cheatsheet-1360w.webp +authors: +- Tarides +source: +--- + +

For developers diving into the OCaml ecosystem, one of the essential tools you'll encounter is odoc. Whether you're a seasoned OCaml programmer or just starting out, understanding how to generate and navigate documentation efficiently is crucial. This is where odoc comes in, OCaml's official documentation generator. To make your experience with odoc even smoother, the odoc team has created the odoc Cheatsheet.

+

What is odoc?

+

odoc is a powerful documentation generator specifically designed for the OCaml programming language. It transforms OCaml interfaces, libraries, and packages into clean, readable HTML, LaTeX, or man pages. If you've worked with JavaDoc or Doxygen in other programming languages, you'll find odoc to be a similarly indispensable tool in the OCaml world.

+

The purpose of odoc is twofold:

+
    +
  1. It helps developers create comprehensive documentation for their projects.
    2. +
  2. It allows users to easily navigate and understand these projects through a standardised format.
    3. +
+

As OCaml projects grow in complexity, well-maintained documentation becomes increasingly important for collaboration, onboarding new team members, and ensuring long-term project sustainability.

+

The odoc Cheatsheet: A Quick Reference for OCaml Developers

+

While odoc is great for generating docs, it uses a syntax that is not widely known. Learning a new syntax can be cumbersome, if not downright difficult. Before this cheatsheet, the resource for the syntax was only in the odoc for Authors page. However, this page offers extensive detail, covering far more than just the syntax. While excellent for in-depth exploration, it can be challenging when you're aiming for quick productivity.

+

The odoc Cheatsheet is a very simple resource for writing simple things. It is easy to read it and discover syntax, and you can use it to recheck your syntax. Rather than explaining, it provides examples, which is less cognitive overhead for the developer. It serves as a concise reference guide that covers the most important aspects of odoc, helping you to quickly get up to speed without wading through extensive documentation.

+

Here’s a closer look at how this cheatsheet benefits you:

+
    +
  1. +

    Easy Access to Essential odoc Syntax +The cheatsheet provides a useful list of odoc syntax. Whether you need to generate documentation for a single module or an entire project, the cheatsheet lays out the exact markup commands you need. This can save a lot of time, as you won’t have to search through various resources to find the correct syntax or options.

    +
    2. +
  2. +

    Concise and Well-Organised Information +Information is presented in a clear, concise table that allows you to quickly find what you need.

    +
    3. +
+

This organisation is particularly beneficial when you’re in the middle of coding and need to find a markup command quickly. The cheatsheet gives you instant access to the most relevant information.

+
    +
  1. A Great Learning Tool for New OCaml Developers +For those new to OCaml, the odoc Cheatsheet doubles as a learning tool. By following the syntax provided, you’ll not only generate better documentation but also gain a deeper understanding of how to structure your code and its corresponding documentation effectively.
    2. +
+

The cheatsheet explains how to use specific annotations in your comments to generate informative documentation. This might not be immediately obvious to someone new to OCaml or odoc, but it can greatly enhance the usability of your generated docs.

+

Conclusion: A Simple and Useful Resource for odoc

+

Whether you're maintaining a large OCaml project or just starting out, the odoc Cheatsheet simplifies the documentation process, making it easier to produce high-quality docs with minimal hassle. Keep this cheatsheet at your fingertips, and ensure your OCaml projects are documented as well as they are coded.

+

So, before you dive into your next OCaml project or documentation task, take a moment to explore the odoc Cheatsheet. It could be the key to making your work more efficient and your documentation more effective.

+ diff --git a/data/planet/tarides/looking-back-on-our-experience-at-icfp.md b/data/planet/tarides/looking-back-on-our-experience-at-icfp.md new file mode 100644 index 0000000000..53fa798fff --- /dev/null +++ b/data/planet/tarides/looking-back-on-our-experience-at-icfp.md @@ -0,0 +1,49 @@ +--- +title: Looking Back on our Experience at ICFP! +description: Spearheading at ICFP 2024, presented six insightful talks, including + new advancements in OCaml on Windows, `opam` 2.2, and interoperable concurrency + projects. +url: https://tarides.com/blog/2024-10-23-looking-back-on-our-experience-at-icfp +date: 2024-10-23T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/milan-evening-1360w.webp +authors: +- Tarides +source: +--- + +

It has been a while since the biggest functional programming event of the year: ICFP 2024 in Milan, Italy. The annual conference, sponsored by ACM SIGPLAN, combines world-class talks with workshops on some of the biggest functional programming languages, including ML, Haskell, OCaml, Scheme and Erlang.

+

Tarides are co-sponsors of ICFP, and several of our team members attend each year. This year, we had six talks given by Tarides team members and many of our colleagues chose to go as participants. I have asked several of them to share their experience at this year's ICFP to give you a taste of what the conference is all about.

+

The Tarides Talks

+

Before we get started, let's recap the talks created or co-created by Tarides engineers and where you can watch them after the fact.

+ +

Experience Reports

+

Curious about ICFP or missing the action already? I've asked several of my fellow Tarides team members who attended ICFP this year to share their thoughts and experiences. Let's dive in!

+

Why ICFP?

+

ICFP stands out to functional programming enthusiasts for gathering a large community of like-minded people in one place. As Jan Midtgaard puts it, "it's a wonderful mix of academics and industry people gathering due to a common interest in functional programming". KC Sivaramakrishnan has been attending ICFP since 2009 when he was a PhD student, and "ICFP is now the place where I meet friends and collaborators as well as the future generation of functional programming researchers".

+

Another reason behind the conference's enduring popularity is, of course, the packed schedule full of high-quality talks. The different tracks offer a variety of opportunities for participants to explore topics that interest them. Ambre Suhamy comments, "I know for sure that I will learn something new and come back from ICFP with more knowledge".

+

Stand-Out Talks

+

On the topic of talks, my colleagues attended several across different days and tracks. I asked them to share some of their impressions from the presentations, and while there were far too many to include them all, let's check out some of what they had to share!

+ +

Memorable Moments

+

My colleagues' week in Milan created several lasting memories. Ambre chaired her first session, the 3rd OCaml Workshop session, which included presentations on Priodomainslib, Saturn, Picos, and Distributed Actors. She also attended FARM, the international workshop on Functional Art, Music, Modelling, and Design. Ambre remembers the workshop as "people using music to make programs, or programming to make music, and understanding music through programming".

+

Tim recalls his many conversations between events with a variety of people in the hallways. It might not be the first thing that springs to mind, but the conversations that strike up organically at ICFP can be enlightening. For example, "people generally didn't know that you could use GBD/LLDB on OCaml binaries and, once they knew that, they were very excited about using those tools on their OCaml programs".

+

KC is focussed on the future, highlighting the feedback he received from participants and how it will help Tarides going forward. "I got some really nice feedback from folks, building on OCaml, about the work that Tarides is doing. I also got lots of honest feedback on what's not working. At the end of the day, our user community matters, and we need to solve their pain points so that OCaml becomes an advantage and not a technical risk for their engineering teams." He also wants to keep contributing to the future of ICFP: "I'm on the ICFP steering committee and will be a DEI co-chair for the next ICFP. I want to ensure that ICFP remains a thriving, friendly, and inclusive place for all of our attendees".

+

Finally, we can't discuss a Milan conference without mentioning the food! All the participants enjoyed sampling the local Italian fare and just look at this delicious pizza!

+

An Italian-style pizza with a whole piece of mozzarella cheese in the middle, surrounded by sliced meat.

+

Join us Next Year!

+

The good news is that ICFP happens every year, so if you didn't attend this year, you can always set your sights on next year. The conference also moves around, alternating locations to make it easier for participants around the globe to join. We look forward to seeing you at ICFP 2025 in Singapore, so come find us if you're going!

+

You can reach out to us on X, Mastodon, Threads, and LinkedIn. Stay in touch!

+ diff --git a/data/planet/tarides/making-crypto-safer-introducing-the-argos-project.md b/data/planet/tarides/making-crypto-safer-introducing-the-argos-project.md new file mode 100644 index 0000000000..8f912297e6 --- /dev/null +++ b/data/planet/tarides/making-crypto-safer-introducing-the-argos-project.md @@ -0,0 +1,36 @@ +--- +title: 'Making Crypto Safer: Introducing the ARGOS Project' +description: A European solution for detecting, evaluating, and tracing suspicious + blockchain transactions is in development by Tarides and partners. +url: https://tarides.com/blog/2024-10-30-making-crypto-safer-introducing-the-argos-project +date: 2024-10-30T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/cryptocurrency-1360w.webp +authors: +- Tarides +source: +--- + +

The world of cryptocurrency and internet transactions is constantly evolving, and the changing landscape of technologies that support this growing industry often means that legislation struggles to keep up, allowing cybercriminals to exploit loopholes and take advantage of the lack of oversight. Concerted effort across the sector is necessary to address this vulnerability.

+

To that end, we are thrilled to announce the ARGOS project, which stands for Analyse et Représentation des Graphes des Opérations Suspectes or the analysis and graphical representation of suspicious operations. Together with Functori, the LMF lab at Paris Saclay, and the Lip6 lab at Sorbonne University, Tarides is creating a platform for blockchain analysis. ARGOS will facilitate the monitoring and tracing of individual transactions on the blockchain, helping both nations enforce the law and organisations comply with regulation.

+

The Current Problem

+

The financial crimes perpetrated using crypto and the blockchain include money laundering, extortion, fraud, and funnelling funding for terrorist activities. Cybercriminals take advantage of the same traits that make crypto attractive to legitimate users: its decentralisation, dynamism, and versatility. Further exacerbating the problem, these same traits make it difficult for nations to legislate and enforce rules like they do for traditional financial institutions like banks.

+

This is because, rather than employing the traditional methods of identification, authentication, and document verification by a central authority, the blockchain uses an 'authorisation by default' approach to validate the exchange itself. Even though existing safeguards exist, which make it possible for police and the judicial system to determine the individuals associated with a transaction, they are not enough to effectively tackle cybercrime. What is needed is a way to identify, analyse, and track suspicious transactions and their sources at scale.

+

The ARGOS Solution

+

Several proposed solutions to the situation exist, but many of them can't address the breadth and complexity of the challenge or/and are not designed for the European financial system. Existing regulations empower nations to pose specific requirements on cryptocurrency providers and traders, and in Europe, that includes PACTE for France. Regulations impose rules on how the blockchain interacts with traditional financial institutions and the obligations that providers have including authenticating clients, freezing accounts, and identifying cryptographic addresses.

+

ARGOS will be a French solution custom-created to comply with and enforce French and European financial market regulations. It is designed to be lightweight enough not to place an undue burden on the existing ecosystem of blockchain developers, cryptocurrency providers, and traders, efficient enough to handle large codebases and complex systems, and robust enough to catch criminal activity reliably.

+

What is ARGOS?

+

The success of ARGOS rests on the key characteristics of the project, which are as follows:

+ +

What Does the Future Hold?

+

The project is in its early stages, and we are collaborating closely with our partners to research and develop new approaches and technologies. Look out for more updates on the project coming in the future!

+

Connect with us online on X, Mastodon, Threads, and LinkedIn to stay updated on our latest projects.

+ diff --git a/data/planet/tarides/making-ocaml-mainstream-support-our-open-source-work-on-github.md b/data/planet/tarides/making-ocaml-mainstream-support-our-open-source-work-on-github.md new file mode 100644 index 0000000000..467e8b0008 --- /dev/null +++ b/data/planet/tarides/making-ocaml-mainstream-support-our-open-source-work-on-github.md @@ -0,0 +1,56 @@ +--- +title: 'Making OCaml Mainstream: Support Our Open Source Work on GitHub' +description: Tarides contributes to the OCaml community with maintenance, community + events, and new features. You can now support this work by sponsoring it on GitHub. +url: https://tarides.com/blog/2024-11-06-making-ocaml-mainstream-support-our-open-source-work-on-github +date: 2024-11-06T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/camel-train-1360w.webp +authors: +- Tarides +source: +--- + +

We are steadfast OCaml advocates, providing core maintenance, hosting community events, and bringing groundbreaking new features to the language. We choose OCaml because it is a programming language with a unique combination of strengths, combining an expressive syntax and strong type system with memory safety and the power of multicore programming.

+

OCaml’s success is the combined result of the innovative efforts, passion, and dedication of the people who contribute to its development. The open-source community behind OCaml works collaboratively and transparently to make OCaml faster, safer, and easier. This community is made up of individual developers, research groups, and companies all working together. Tarides is one of the companies that contribute extensively to OCaml, and several of our team members are core OCaml developers.

+

You can support our open-source work by becoming a sponsor on our GitHub page. Your contribution will have a direct impact on the OCaml ecosystem by helping us maintain, develop, and improve its libraries, features, and tools. Let’s show you what we’re working on and what your support will help us achieve for OCaml!

+

What Does Tarides do?

+

At Tarides, we’re passionate about making OCaml even more powerful and accessible for developers. Our work focuses on three key areas: Enhancements, maintenance, and accessibility. Your contribution will support our work in all these areas.

+
    +
  1. Enhancing the Language: We bring new features to OCaml by resolving developer pain points and testing performance on different platforms. We want OCaml to be a competitive programming language with developer experience a high priority.
    2. +
  2. Maintaining Core Tools and Libraries: We ensure that OCaml developers have a reliable foundation for their projects by keeping the tools and libraries they depend on up to date.
    3. +
  3. Community Support and Outreach: We prioritise clear documentation and tutorials to improve accessibility and regularly organise events that allow community members to meet and exchange ideas.
    4. +
+

What Projects Does Tarides Work on?

+

We work on a broad range of projects targeting different parts of the OCaml ecosystem: Compiler and language tools, development tools, community and infrastructure, and advanced projects.

+

Compiler and Language Tools

+ +

Development Tools

+ +

Community and Infrastructure

+ +

Advanced Projects

+ +

Contribute to the Future of OCaml Today!

+

By sponsoring us, you’ll support the maintenance of these essential OCaml tools and libraries and contribute to the growth of a diverse, dynamic community. Your contribution will have a direct impact on our projects and the OCaml ecosystem as a whole.

+

Please reach out to us on X, Mastodon, Threads, and LinkedIn. We look forward to hearing from you!

+ diff --git a/data/planet/tarides/monoculture-of-insecurity-how-crowdstrikes-outage-exposes-the-risks-of-unchecked-complexity-in-cybersecurity.md b/data/planet/tarides/monoculture-of-insecurity-how-crowdstrikes-outage-exposes-the-risks-of-unchecked-complexity-in-cybersecurity.md new file mode 100644 index 0000000000..8463644385 --- /dev/null +++ b/data/planet/tarides/monoculture-of-insecurity-how-crowdstrikes-outage-exposes-the-risks-of-unchecked-complexity-in-cybersecurity.md @@ -0,0 +1,44 @@ +--- +title: 'Monoculture of Insecurity: How CrowdStrike''s Outage Exposes the Risks of + Unchecked Complexity in Cybersecurity' +description: Explore how structured development practices and technologies like unikernels + and OCaml can mitigate cyber risks, as highlighted by recent industry disruptions. +url: https://tarides.com/blog/2024-08-01-monoculture-of-insecurity-how-crowdstrike-s-outage-exposes-the-risks-of-unchecked-complexity-in-cybersecurity +date: 2024-08-01T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/Blue-Screen-1360w.webp +authors: +- Tarides +source: +--- + +

A seismic event in the IT world, everyone is talking about the CrowdStrike update that caused global chaos earlier this month. There are many great articles and blog posts dissecting the event and suggesting ways to avoid a repeat. Rather than join our voice to the chorus and explain how a small change could have avoided the entire palaver, we will approach the topic more broadly.

+

While it is helpful to understand what happened with CrowdStrike, the next major outage will likely arise from a different flaw altogether. As such, and since we expect that another major event is likely to come, it’s essential to consider the risk factors behind these major cyber events and ways to reduce those risks.

+

The cybersecurity sector is constantly facing new threats and challenges. How can we transform these obstacles into opportunities for growth and improvement, ensuring greater protection for those who rely on our services? This blog post explores the answers to this question, presenting some lesser-known solutions that deserve consideration, and providing a fresh perspective on staying ahead of emerging threats and building more resilient defences.

+

What we Know so far

+

Affecting at least 8.5 million Windows machines, the outage significantly affected the aviation, broadcasting, and healthcare industry. The BBC labelled it “probably the largest ever cyber-event” and “one of the worst cyber-incidents in history.” But what actually happened?

+

Arising from something as commonplace as a software update for the Falcon platform, CrowdStrike’s own preliminary Post Incident Review, indicates that a security content configuration update delivered an undetected error (the now infamous Channel File 291) to user machines. The error slipped through the validation checks due to a bug, and trust in the tests allowed a faulty file with an out-of-bounds memory error to reach production. At its root, the global outage appears to be caused by unsafe parsers (a classic error), resulting in a parsing bug.

+

What are the Best Practices for the Cybersecurity Sector?

+

Now that we’ve covered this background, it’s time to look at some of the underlying factors that played a role in the CrowdStrike outage and the ones yet to come. The global outage served as an excellent wake-up call to the entire industry about the necessity of maintaining the checks and balances that keep our global systems secure.

+

Supply Chain Delivery

+

Let’s start with the fundamentals: how did the flawed update get delivered to so many? When deploying updates at scale, industry best practices can help mitigate risks by employing methods like staggered deployments and rollback options. In a best-case scenario updates are staggered, or rolled out incrementally, starting with 1% and, if all goes well, 5%, and so on. One can also use automated systems that rollback updates when a fault is detected, undoing the damage and keeping user’s machines operational. By using either method, preferably both in combination, a flaw in an update has negligible impact, voiding the kind of international chaos we saw on Friday.

+

Another critical aspect of the supply chain is the internal testing performed before deployment to ensure quality and safety. The recent chaos would likely have been preventable if the internal testing processes had caught the flaw earlier.While cost-cutting measures may be tempting, they can ultimately lead to much greater costs in the event of a cybersecurity breach or production downtime.

+

OS Monocultures: Do you Really Need a Full Windows OS Stack to run an Airport Screen?

+

The IT industry is increasingly dominated by a few major operating systems, primarily Microsoft Windows. This creates the emergence of 'OS monocultures', with one dominant provider overshadowing a few large ones (Linux and Mac), leaving little space for diverse, smaller suppliers. While these monocultures offer benefits, they also pose significant risks, and any introduced vulnerabilities can cause widespread damage.

+

This is what happened with CrowdStrike. The cybersecurity firm has around 20% market share, and because everyone uses the same stack, a single bug can have an enormous impact. One way to reduce the risk of a shared stack is to generate a unique stack for each application; that way, bugs are contained in that stack. One way of achieving this is by using unikernels to build a small, highly specified stack with only what is required to run the application. MirageOS is a library operating system that constructs unikernels to create secure, high-performance network applications with small attack surfaces.You don’t actually need to install a generic operating system to manage a single-purpose appliance, such as an airport screen.

+

Formal Verification, Testing, and Organisational Change

+

The road to security and reliability is paved with organisational changes that improve the overall stability of systems and reduce risk, impacting the way we develop software from start to finish. Scott Hanselmann, the VP of Developer Community at Microsoft, highlights this dynamic in one of his posts on X:

+
+

“It’s always one line of code, but it’s NEVER one person... Engineering practices failed to find a bug multiple times, regardless of the seniority of the human who checked that code in. Solving the larger system thinking SDLC matters more than the null pointer check.”

+
+

But what does changing the software development life cycle on an organisational level look like? For one, it involves spending the time and cost of creating comprehensive tests that catch bugs easily missed by developers before they ever reach production.

+

Including formal verification, for example of the device driver and the code it executes, is another aspect of software development that can prevent faults reaching production. Using formal verification, developers can mathematically prove that a program behaves according to its formal model and correctly performs a defined property.

+

As it relates to the CrowdStrike incident, formal verification of parsers is challenging but not impossible. For example, the EverParse framework emits secure, formally verified code for parsers that can be used in programs, including OCaml programs. Creating a software development culture that includes formal verification, fuzz testing, and other tests decreases the risk of failures slipping through the net.

+

The Role of Type Safety

+

Finally, let’s look at perhaps a more obvious topic in the light of the fault in Channel File 291. Using type- and memory-safe languages, like OCaml and Rust, prevents out-of-bounds memory errors and a whole class of other bugs.

+

That’s not the key takeaway we can all learn from, however, which is about complexity. The assertion that “the central enemy of reliability is complexity ... complex systems tend to not be entirely understood by anyone” from a cybersecurity paper authored by several industry specialists holds true in this case. By eliminating a whole class of errors at compile time, a language like OCaml with a strong type system critically reduces the kind of complexity that leads to cyber-insecurity. A language like OCaml simplifies the developer workflow when it comes to catching bugs.

+

Most importantly, from an industry standpoint, and as mentioned above, the faulty file that caused the outage remained undetected , even in the face of extensive stress tests. Building critical systems with secure-by-design principles includes using building blocks that contribute to the robustness of the entire system by preventing faults and reducing complexity. One facet of this puzzle is to use languages immune to certain kinds of bugs, such as type- and memory-safe languages, but that is not enough. Varied and rigorous tests, like fuzz testing, are a necessary complement to any language. For example, the MirageOS network stack has had fuzz testing performed on it to prevent parser issues, providing another layer of safety to the already type-safe OCaml.

+

Join in the Conversation

+

In essence, the cause and lessons from the CrowStrike outage are more complex than they may seem at first glance. It’s easy to reduce it to a line of faulty code, but the real takeaway is that the entire industry needs to implement better practices to safeguard users from risk. This outage was not the result of a cyber attack or malware, but the next one could be, and we cannot let the fate of our global networks rest entirely on endpoint security measures like antivirus programs, firewall management, and VPNs. We need to build foundational secure systems from the ground up.

+

In this context, and in light of global calls for change in how cybersecurity is addressed, it is the right time to have these conversations and strengthen the sector from within. We believe the best approach is to adopt a secure-by-design strategy implemented in a type-safe and reliable language like OCaml.

+

There are many perspectives on this, however, and we want to hear yours. Connect with us on X (formerly Twitter) and LinkedIn and share your thoughts – we look forward to hearing from you!

+ diff --git a/data/planet/tarides/ocaml-compiler-manual-html-generation.md b/data/planet/tarides/ocaml-compiler-manual-html-generation.md new file mode 100644 index 0000000000..7dca3b32dd --- /dev/null +++ b/data/planet/tarides/ocaml-compiler-manual-html-generation.md @@ -0,0 +1,99 @@ +--- +title: OCaml Compiler Manual HTML Generation +description: Enhanced OCaml Manual URLs for better readability and version-specific + references, providing a seamless user experience and improving backlink quality. +url: https://tarides.com/blog/2024-07-17-ocaml-compiler-manual-html-generation +date: 2024-07-17T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/compiler-manual-1360w.webp +authors: +- Tarides +source: +--- + +

In order to avoid long, confusing URLs on the OCaml Manual pages, we set out to create a solution that shortens these URLs, including section references, and contains the specific version. The result improves readability and user experience. This article outlines the motivation behind these changes and how we implemented them.

+

Challenge

+

The OCaml HTML manuals have URL references such as https://v2.ocaml.org/manual/types.html#sss:typexpr-sharp-types, and they do not refer to any specific compiler version. We needed a way to easily share a link with the version number included. The OCaml.org page already has a mention of the compiler version, but it refers to specific https://ocaml.org/releases.

+

We wanted a canonical naming convention that is consistent with current and future manual releases. It would also be beneficial to have only one place to store all the manuals, and the users of OCaml.org should never see redirecting URLs in the browser. This will greatly help increase the overall backlink quality when people share the links in conversations, tutorials, blogs, and on the Web. A preferred naming scheme should be something like:

+

https://v2.ocaml.org/releases/latest/manual/attributes.html +https://v2.ocaml.org/releases/4.12/manual/attributes.html

+

Using this, we redirected the v2.ocaml.org to OCaml.org for the production deployment. Also, the changes help in shorter URLs that can be easily remembered and shared. The rel="canonical" is a perfectly good way to make sure only https://ocaml.org/manual/latest gets indexed.

+

Implementation

+

After a detailed discussion, the following UI mockup to switch manuals was provided via GitHub issue, and Option A was selected.

+

UI Mockup

+

Our proposed changes to the URL are shown below:

+

Current: https://v2.ocaml.org/releases/5.1/htmlman/index.html
+Suggested: https://ocaml.org/manual/5.3.0/index.html

+

Current: https://v2.ocaml.org/releases/5.1/api/Atomic.html
+Suggested: https://ocaml.org/manual/5.3.0/api/Atomic.html

+

HTML Compiler Manuals

+

The HTML manual files are hosted in a separate GitHub repository at https://github.com/ocaml-web/html-compiler-manuals/. It contains a folder for each compiler version, and it also has the manual HTML files.

+

A script to automate the process of generating the HTML manuals is also available at https://github.com/ocaml-web/html-compiler-manuals/blob/main/scripts/build-compiler-html-manuals.sh. The script defines two variables, DIR and OCAML_VERSION, where you can specify the location to build the manual and the compiler version to use. It then clones the ocaml/ocaml repository, switches to the specific compiler branch, builds the compiler, and then generates the manuals. The actual commands are listed below for reference:

+
echo "Clone ocaml repository ..."
+git clone git@github.com:ocaml/ocaml.git
+
+# Switch to ocaml branch
+echo "Checkout $OCAML_VERSION branch in ocaml ..."
+cd ocaml
+git checkout $OCAML_VERSION
+
+# Remove any stale files
+echo "Running make clean"
+make clean
+git clean -f -x
+
+# Configure and build
+echo "Running configure and make ..."
+./configure
+make
+
+# Build web
+echo "Generating manuals ..."
+cd manual
+make web
+
+

As per the new API requirements, the manual/src/html_processing/Makefile variables are updated as follows:

+
WEBDIRMAN = $(WEDBIR)/$(VERSION)
+WEBDIRAPI = $(WEBDIRMAN)/API
+
+

Accordingly, we have also updated the manual/src/html_processing/src/common.ml.in file OCaml variables to reflect the required changes:

+

+let web_dir = Filename.parent_dir_name // "webman" // ocaml_version
+
+let docs_maindir = web_dir
+
+let api_page_url = "api"
+
+let manual_page_url = ".."
+
+

We also include the https://plausible.ci.dev/js/script.js script to collect view metrics for the HTML pages. The manuals from 3.12 through 5.2 are now available in the https://github.com/ocaml-web/html-compiler-manuals/tree/main GitHub repository.

+

OCaml.org

+

The OCaml.org Dockerfile has a step included to clone the HTML manuals and perform an automated production deployment as shown below:

+
RUN git clone https://github.com/ocaml-web/html-compiler-manuals /manual
+
+ENV OCAMLORG_MANUAL_PATH /manual
+
+

The path to the new GitHub repository has been updated in the configuration file, along with the explicit URL paths to the respective manuals. The v2 URLs from the data/releases/*.md file have been replaced without the v2 URLs, and the manual /releases/ redirects have been removed from redirection.ml. The /releases/ redirects are now handled in middleware.ml. The caddy configuration to allow the redirection of v2.ocaml.org can be implemented as follows:

+
v2.ocaml.org {
+	redir https://ocaml.org{uri} permanent
+}
+
+

Call to Action

+

You are encouraged to checkout the latest OCaml compiler from trunk and use the build-compiler-html-manual.sh script to generate the HTML documentation.

+

Please do report any errors or issues that you face at the following GitHub repository: https://github.com/ocaml-web/html-compiler-manuals/issues

+

If you are interested in working on OCaml.org, please message us on the OCaml Discord server or reach out to the contributors in GitHub.

+

References

+
    +
  1. +

    (cross-ref) Online OCaml Manual: there should be an easy way to get a fixed-version URL. https://github.com/ocaml/ocaml.org/issues/534

    +
    2. +
  2. +

    Use webman/*.html and webman/api for OCaml.org manuals. https://github.com/ocaml/ocaml/pull/12976

    +
    3. +
  3. +

    Serve OCaml Compiler Manuals. https://github.com/ocaml/ocaml.org/pull/2150

    +
    4. +
  4. +

    Simplify and extend /releases/ redirects from legacy v2.ocaml.org URLs. https://github.com/ocaml/ocaml.org/pull/2448

    +
    5. +
+ diff --git a/data/planet/tarides/project-wide-occurrences-a-new-navigation-feature-for-ocaml-52-users.md b/data/planet/tarides/project-wide-occurrences-a-new-navigation-feature-for-ocaml-52-users.md new file mode 100644 index 0000000000..87d03a0f68 --- /dev/null +++ b/data/planet/tarides/project-wide-occurrences-a-new-navigation-feature-for-ocaml-52-users.md @@ -0,0 +1,153 @@ +--- +title: 'Project-Wide Occurrences: A New Navigation Feature for OCaml 5.2 Users' +description: Achieved project-wide occurrences search in OCaml's editor tooling with + `merlin-lib` 5.1-502 update, enabling cross-file identifier usage queries. +url: https://tarides.com/blog/2024-08-28-project-wide-occurrences-a-new-navigation-feature-for-ocaml-5-2-users +date: 2024-08-28T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/camls_2-1360w.webp +authors: +- Tarides +source: +--- + +

With the release of merlin-lib 5.1-502 and associated ocaml-lsp-server, we +brought a new, exciting feature to OCaml's editor tooling: project-wide +occurrences.

+

The traditional "occurrences" query in Merlin modes, named "Find All +References" in LSP-based mode, was used to only return results in the active buffer. +This is no longer the case!

+

Occurrences queries will now return every usage of +the selected identifier across all of the project's source files.

+
+

There are some limitations that come with this initial release. When queried +from an identifier's usage or its definition, all other usages of it +are returned, but related declarations are not. In particular, this means +that queries should be made from implementation files, not interfaces (.mli).

+
+

In this post, we will give an overview of the ecosystem's various parts that +need to work together for this feature to work.

+

Try It!

+

Before diving into technical details, let's see how it works. You can try it on any project that builds with Dune and is compatible with OCaml 5.2.

+

Update your switch by running opam update && opam upgrade to get the required tool versions:

+ +

Since we are looking for all occurrences, we need to build an index for Merlin +and LSP. Fortunately, this is well integrated in Dune, and you can build the index +for your project by running:

+
dune build @ocaml-index
+
+

This alias ensures that all the artifacts needed by Merlin are built. You can +also add --watch to always keep the configuration and the indexes up to date +while you edit your source files.

+
+

Note that unlike dune build @check, the @ocaml-index will build the entire project, including tests.

+
+

Once the index is ready, you can query for project-wide occurrences:

+ +

Here is a comparison of a references query before, and after building the index:

+
+ +
+

Now, let's dive into more technical details.

+

High-Level Overview

+

The base design is fairly simple. We want to iterate on every identifier of +every source file, determine their definition, and group together those that +share the same definition. This forms an index. Tools can then query that index +to get the location list of identifiers that share the same definition.

+

The following section describes how we implemented that workflow:

+
    +
  1. Compute definitions using two-step shape reduction
    2. +
  2. Driving of the indexer tool by the build system
    3. +
  3. Changes to Merlin to properly answer queries
    4. +
+

Two-Step Shape Reduction

+

Finding an identifier's definition in OCaml is a difficult problem, mostly +because of its powerful module system. A solution to this problem has been recently described +in a presentation at the ML +Workshop: shapes. +In short, shapes are terms of a simple lambda-calculus that represent an +abstraction of the module system. To find an identifier's definition, one +can build a shape from its path and reduce (as in beta-reduction) that shape. +The result should be a leaf with a UID that uniquely represents the +definition.

+

This has been implemented in the compiler, and Merlin already takes advantage of +it to provide a precise jump-to-definition feature.

+

For project-wide occurrences, we perform shape reduction in two steps:

+

First, at the end of a module's compilation, the compiler iterates on the +Typedtree and locally reduces every identifier's shape. If the +identifier is locally (in the same unit) defined, the result will be a +fully-reduced shape holding the definition's UID. However, if the identifier is +identified in another compilation unit, the result is a partially-reduced +shape, because we cannot load the .cmt files of other compilation +units (that are required to finish the reduction) without breaking the +separate compilation assumptions. These resulting UIDs or partially-reduced +shapes are stored in the unit's .cmt file:

+
type cmt_infos = {
+  ...
+  cmt_ident_occurrences :
+    (ident_with_loc * def_uid_or_shape) list
+}
+
+

Then, an external tool (called ocaml-index) will read that list and finish +the reduction of the shapes when necessary. This step might load the .cmt files +of any transitive dependency the unit relies on.

+

Indexation by the Build System

+

The tool we just introduced, ocaml-index, plays two roles:

+
    +
  1. It finishes the reduction of the shapes stored in the .cmt files.
    2. +
  2. It aggregates locations that share the same definition's UID.
    3. +
+

The result is an index that is written to a file. Additionally, the tool +can merge multiple indexes together. This allows build systems to handle +indexation in the way they decide.

+

We only provide rules for Dune right now, but the tools themselves are built +system agnostic. The Dune rules are as follow:

+

For every stanza library or executable, we index every .cmt file and store +the results into an index file for the stanza.

+ +

This is a somewhat simple but heavy process, and it could be refined in the future. Right now it performs well enough to provide a usable watch mode in small to fairly large projects (like Dune itself).

+

Index Configuration and Reading

+

Last but not least, we need a way for Merlin to know were the index files are +located and how to read them.

+

This is done by using a new configuration directive INDEX. It can be used to +provide one or more index files to Merlin. Then, querying for all the usages of +the identifier under the cursor is done in the following way:

+ +

Future Work

+

Thank you for reading this post! We hope you will have a lot of fun exploring +your codebases using this new feature. We have a lot of exciting improvements on +our roadmap, some of which involve returning the declarations linked to an +identifier and providing project-wide renaming queries.

+

If you are interested to learn more about these features or to contribute, +please have a look at this tracking +issue. You can also have a look at +the +announcement +and wiki +page. +Finally, feel free to attend future Merlin public +meetings and +watch the talk at the OCaml +Workshop +during ICFP!

+ diff --git a/data/planet/tarides/summer-of-internships-projects-from-the-ocaml-compiler-team.md b/data/planet/tarides/summer-of-internships-projects-from-the-ocaml-compiler-team.md new file mode 100644 index 0000000000..2af6bc9e2c --- /dev/null +++ b/data/planet/tarides/summer-of-internships-projects-from-the-ocaml-compiler-team.md @@ -0,0 +1,36 @@ +--- +title: 'Summer of Internships: Projects From the OCaml Compiler Team' +description: Interns modularised the Olly tool, created eBPF-based performance monitoring, + improved OCaml's package management, and enhanced Ortac for better testing. +url: https://tarides.com/blog/2024-09-24-summer-of-internships-projects-from-the-ocaml-compiler-team +date: 2024-09-24T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/rowers-team-1360w.webp +authors: +- Tarides +source: +--- + +

We have had the pleasure of hosting several interns in the compiler team this past year. Their projects have tackled varied and challenging tasks touching on different aspects of compiler development, ranging from modularising the observability tool Olly to creating eBPF-based kernel-side performance monitoring, improving polyglot package management, and lifting limitations of the Ortac tool that helps developers test Gospel specifications for OCaml.

+

Let's take a look at what the interns have been up to over the past six months. Remember, if you want to intern with us, keep an eye on our careers page for upcoming opportunities!

+

Eutro and Olly

+

@eutro's internship focussed on making the observability tool Olly more useful for developers by addressing two shortcomings: an incompatibility between Olly and the Runtime Events API that would cause crashes in certain cases, and the number of Olly's dependencies which made it difficult or impossible to use its core functions with unreleased ("trunk") OCaml (or at all on Windows). To resolve these issues, @eutro modularised Olly, implementing a table-based translation of runtime event names and tags.

+

@eutro modularised Olly by refactoring the binary into smaller libraries, with the awkward dependencies isolated into an optional library. Splitting up the libraries gives users greater control over their dependencies and you can learn more about modularisation in the PR.

+

The second part of the internship focussed on the table-based translation of runtime event names and tags to allow different versions of OCaml to consume runtime events. The goal was to avoid two bugs that arose when Olly profiles a program compiled with a different version of OCaml, olly trace generating nonsensical names for the slices and olly gc-stats silently generating garbage output. To delve into the details, check out @eutro's PR about runtime event names.

+

Lastly, @eutro managed to squeeze in some bug-fixes as well! One PR addresses the incorrect use of snprintf_os in formatting the runtime events ring file path and another that fixes some memory bugs in runtime_events_consumer.c. Both of these fixes will be included in the 5.3 OCaml update.

+

Lee Koon Wen and Eio

+

The Eio library enables users to write high-performance I/O programs leveraging the new effects system that came with OCaml 5. The I/O library pairs well with the io_uring interface on Linux as a rule; however, the asynchronous nature of io_uring can make it hard for the developer to get a grasp on the performance of their Eio programs when they are bottlenecked by something within the kernel rather than the program itself.

+

The Linux kernel has a mature and extensive system for gathering data on its performance. In his internship project, Lee Koon Wen's task was to produce a library that used the Linux eBPF probes to gather kernel-side data on an Eio program's io_uring use and deliver them to the program's runtime events. This would let users analyse kernel-side performance data alongside their program's performance using an observability tool like Olly.

+

Two projects have sprung from this work, uring-trace and ocaml-libbpf. The former is a tracer that, using bindings provided by the latter, can extract events from a Linux kernel. These traces can then be generated in Fuschia format and displayed on Perfetto. This project will benefit developers on the Linux platform, helping them understand and optimise their programs using accurate data.

+

Ryan and Polyglot Package Management

+

Using several programming languages in one project lets you take advantage of the particular strengths of each language and of its library ecosystem. For example, Python is well-known for its data science libraries, Rust for its ownership memory model, and OCaml for its type safety. Over the past couple of decades, many large programming language ecosystems (and even some smaller ones) have acquired language-specific package managers, e.g. pip (Python's; 2008), cargo (Rust's; 2015 - although it started with one) and, of course, opam (OCaml's; 2013). Managing these so-called 'polyglot programming' projects, with several languages working together, relies on coordinating these package managers to provide language libraries and toolchains like compilers and build systems. The need to use multiple package managers naturally increases the complexity of these projects. Additionally, dependencies are hard, or impossible, to express across different package managers.

+

Ryan Gibb's research internship at Tarides focussed on using nix as an initial bridge towards these objectives, extending opam to support the provision of "external dependencies" using Nix, the language-agnostic functional package manager, instead of the OS's own package manager. There has been much work in this area already (e.g. opam-nix and opam2nix), but these have focussed more on being able to take opam packages themselves and install them using nix.

+

Ryan's work moves in the other direction, allowing Nix packages to be used within the environment set-up by opam, by adding a depext mechanism to opam. Parallel with this work, Ryan also extended a previous investigation with nixpkgs to allow users to be able to specify versions of Nix dependencies. In general, Nix only supports the latest versions, but by analysing nixpkgs repository history we can map the versions of the packages we’re interested in to the ranges in nixpkgs commit history which provide them. Using opam’s solver we can then find the maximum commit of nixpkgs satisfying the version constraints on the packages (as long as a state exists meeting the conditions).

+

Future work will address current limitations and bring improvements to the workflow for users. For example, opam’s Nix depext mechanism picks up the environment variables from the builder's shell, meaning it must manually specify the environment it wants to extract. It may be possible to access the env attribute of derivations directly as the Nix binary does. Ryan intends to keep working on these limitations as well as future goals, including shepherding Opam's Nix depext support through review and possibly productionising opam-nix-repository for use in opam-repository.

+

For more information, check out the project's PRs, #5982 and #2.

+

Nikolaus, Gospel and Ortac

+

The culture around OCaml values safety and reliability, so it is no surprise that a suite of tools has been developed to ensure these qualities. One such tool, Gospel, is a contract-based behavioural specification language that can provide a logical model for OCaml types and describe the intended behaviour of functions using pre- and post-conditions. Ortac, in turn, is a tool that can generate a QCheck-STM test suite based on the Gospel specification of a library. You can find out more about them in the dedicated post Getting Specific: Announcing the Gospel and Ortac Projects.

+

The goal of Nikolaus Huber's internship was to lift some of the limitations of Ortac and QCheck-STM to expand its use cases for developers. It's essential to increase the types of tests that users can generate so that more OCaml code can be checked using Gospel. His project has produced three PRs, #235 which centres on allowing tests to run without system under test in the signature, #237 focusses on adding support for tests with tuples in their signature, and #247 aiming to introduce support for testing functions with multiple systems under test as arguments.

+

In addition to the PRs addressing Ortac limitations, Nikolaus has also fixed several issues regarding Gospel and Ortac. He added a new error for when there are no commands produced during the translation from Gospel to OCaml, fixed a bug within the QCheck-STM that occurred when testing functions that return integers, and addressed another bug where a type check would incorrectly indicate that code was correct. All in all, Nikolaus' project benefits developers who want to test their OCaml programs to ensure they perform predictably and correctly.

+

Stay in Touch

+

We want to hear from you! Follow us on X, Mastodon, Threads, and LinkedIn for the latest news from Tarides and to share your thoughts with us. Are you interested in completing an internship project with us? Keep an eye on our careers page, where we announce upcoming internship opportunities. Happy hacking!

+ diff --git a/data/planet/tarides/the-biggest-functional-programming-conference-of-the-year-what-are-we-bringing-to-icfp.md b/data/planet/tarides/the-biggest-functional-programming-conference-of-the-year-what-are-we-bringing-to-icfp.md new file mode 100644 index 0000000000..52222e62aa --- /dev/null +++ b/data/planet/tarides/the-biggest-functional-programming-conference-of-the-year-what-are-we-bringing-to-icfp.md @@ -0,0 +1,44 @@ +--- +title: 'The Biggest Functional Programming Conference of the Year: What are we Bringing + to ICFP?' +description: Discover Tarides' impactful talks at ICFP 2024, featuring advancements + in OCaml interoperability, Windows support, and verified concurrent data structures. +url: https://tarides.com/blog/2024-08-30-the-biggest-functional-programming-conference-of-the-year-what-are-we-bringing-to-icfp +date: 2024-08-30T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/Milan-icfp1-1360w.webp +authors: +- Tarides +source: +--- + +

Feeling fashionable? Milan is calling! ICFP 2024 will be held in the Italian fashion capital from 2-7 September, and there is something there for everyone to enjoy. The ACM SIGPLAN International Conference on Functional Programming is a yearly highlight with various keynotes, tutorials, and tracks to discover.

+

Can't wait for September 2nd? Check out the talks we're bringing to the conference this year and get a taste of what's to come!

+

Tarides Talks

+

We are excited about all the talks at the OCaml Workshop this year, and it's great to see such a variety of topics being presented. You can browse all the accepted papers on the OCaml track of the ICFP website. This year, Tarides team members will give five talks at the OCaml workshop and one at the ML workshop, so let's dive into the topics!

+

Wasm_of_ocaml at the ML Workshop by Jérôme Vouillon

+

Jérôme Vouillon will be presenting on the fork of the well-loved Js_of_ocaml compiler, Wasm_of_ocaml, which translates OCaml bytecode to WebAssembly (Wasm) rather than to JavaScript. Wasm is a low-level virtual machine that is both platform- and language-independent and is attractive to developers as a portable compilation target deployable on a wide variety of platforms. Wasm_of_ocaml is already fairly mature, having been successfully used on large programs.

+

Curious about what this means for OCaml users? Jérôme's talk will give you an overview of the compiler's features, including that it's highly compatible with Js_of_ocaml (one can compile existing programs with minimal changes) and offers a performance boost over the same (2x or more!). In addition, the talk will give you some background to Wasm_of_ocaml's design, the implementation of its runtime environment, how it interacts with JavaScript APIs, how we can take advantage of JavaScript to implement functionalities that are currently unavailable in Wasm, and share some benchmarks to give you an idea of how the compiler performs. Check out Jérôme's talk in the ML track for all this and more!

+

First-Class Windows: Building a Roadmap for OCaml on Windows by Sudha Parimala, Benjamin Canou, Pierre Boutillier, and David Allsopp

+

The goal of the First-Class Windows team (which we discuss more in our blog post introducing the project is to bring support for the Windows platform up-to-par with Tier-1 platforms like Linux and macOS. Reaching this milestone will require planning, collaboration, and iterative change. Still, we expect the process will significantly enhance the OCaml experience for many users. +Check out the talk at the OCaml Workshop track at ICFP to learn all about the project's background, the current state of OCaml on Windows, the launch of the Windows Working Group, what information they are gathering, and where the project is heading.

+

Most importantly, the talk will unveil the new roadmap, which outlines the plan for addressing the pain points and improving OCaml on Windows. The roadmap is intended as a living, collaborative document. Join the talk to be part of the discussion and improve OCaml on Windows!

+

Project-Wide Occurrences for OCaml: A Progress Report by Ulysse Gérard

+

Our next talk will be great news for anyone who writes programs for OCaml! Good editor tooling is indispensable when writing programs, and different language servers provide a variety of features.

+

Before the OCaml 5.2 update, the main language servers were limited to providing occurrences inside the active buffer. After the update with the latest Dune, Merlin, and ocaml-lsp servers, users can take advantage of a new feature enabling project-wide usages search. It allows users to list all the occurrences of a given value, type, or module, quickly navigating between each instance.

+

The team prioritised three key areas when developing the feature: correctness, exhaustivity, and performance. Correctness refers to the tool's ability to list the occurrences of a value without including false positives; exhaustivity refers to the fact that it needs to list all occurrences and perform the way it yields these results in a reasonable amount of time.

+

Come to the talk for a demonstration of the powerful new search features available in OCaml! Learn about the project's design and implementation, the challenges they encountered (including some noteworthy patches to the compiler, Dune, Merlin, and ocaml-lsp!), and improvements planned for the future.

+

Picos – Interoperable Effects-Based Concurrency by Vesa Karvonen

+

Picos is an ongoing project created to allow users to mix and match effects-based concurrent programming libraries and async I/Os. OCaml 5 introduced support for parallelism and effects, which enables the implementation of direct-style cooperative concurrency libraries like Eio. In fact, many such libraries have been created, including Moonpool, Domainslib, Miou, and more!

+

The current difficulty is that all of these libraries are incompatible, meaning that a program that uses one cannot directly use another. This also means that, theoretically, libraries would need to provide an ever-increasing number of backends to ensure their users could combine them with the effects-based scheduler of their choice. This constant game of catch-up isn't desirable for developers or users of these libraries, and Picos aims to solve this problem.

+

Picos is an interface that enables interoperability between different libraries, created to provide users with greater flexibility and choice. Vesa's talk will introduce the nature of the problem, technical details of how Picos is implemented, details about its performance, and a vision for the future of schedulers in OCaml with Picos.

+

Opam 2.2 and Beyond by Raja Boujbel, Kate Deplaix, and David Allsopp

+

The hardworking team behind opam 2.2 are excited to present the update and share the new features! The update's main feature is native Windows support, something many community members have been looking forward to. With the project commencing in 2014, it has taken a significant amount of work and a long time to reach this important milestone – a process you can learn all about in their upcoming talk!

+

The talk will give listeners an opportunity to understand all the different elements that came together to bring native Windows support to OCaml, along with some of the other new features added in opam 2.2. This includes often overlooked aspects of releases like bug fixes and functional testing for stability.

+

Additionally, the talk presents insights into the maintenance of opam and moving towards a new release cycle, hinting at what the future will bring. If you're at all curious about opam and how maintainers bring new features to users, this is the talk for you!

+

Saturn: A Library of Verified Concurrent Data Structures for OCaml 5 by Clément Allain, Vesa Karvonen, Carine Morel

+

This talk presents a useful new OCaml 5 library that offers a collection of ready-made efficient concurrent data structures that are well-tested, benchmarked, and, in part, formally verified.

+

Parallel programs are complex, and sharing data between multiple threads presents a well-known difficulty. Using locks is a known way of managing this complexity, but it is not always the best option, potentially introducing unsatisfactory performance and liveness issues. In such cases, lock-free implementations may be preferable, but their complexity can make them hard to design. Saturn saves the OCaml 5 developer the trouble of designing their own lock-based or lock-free data structures by providing them with a selection of standard ready-to-use structures.

+

Join the talk to hear all about the library's design and details about the benchmarks, tests, and formal verification the team has done. You can look forward to a technical deep dive full of details about what creating parallel programs in OCaml really involves!

+

Until Next Time!

+

If you're attending ICFP this year, come and find us! We would love to chat with you about everything OCaml and functional programming. To stay up-to-date, you should follow us on LinkedIn and X. We look forward to hearing from you!

+ diff --git a/data/planet/tarides/unlock-your-teams-potential-with-expert-training-in-ocaml-cybersecurity-fundamentals-functional-programming-and-more.md b/data/planet/tarides/unlock-your-teams-potential-with-expert-training-in-ocaml-cybersecurity-fundamentals-functional-programming-and-more.md new file mode 100644 index 0000000000..396f34a9b8 --- /dev/null +++ b/data/planet/tarides/unlock-your-teams-potential-with-expert-training-in-ocaml-cybersecurity-fundamentals-functional-programming-and-more.md @@ -0,0 +1,55 @@ +--- +title: "Unlock your Team\u2019s Potential with Expert Training in OCaml, Cybersecurity + Fundamentals, Functional Programming, and More" +description: Explore how Tarides enhances team capabilities with bespoke training + courses based on OCaml expertise, offering flexible learning and post-training support. +url: https://tarides.com/blog/2024-10-01-unlock-your-team-s-potential-with-expert-training-in-ocaml-cybersecurity-fundamentals-functional-programming-and-more +date: 2024-10-01T00:00:00-00:00 +preview_image: https://tarides.com/blog/images/aeroplanes-1360w.webp +authors: +- Tarides +source: +--- + +

Training your teams has proven benefits, enhancing the efficiency and quality of work, and equipping members with the skills they need to tackle new challenges. Specialist training empowers them to use new techniques, leverage advanced technologies, and solve more complex problems.

+

At Tarides, we are launching a new initiative to share our expertise and industry experience in a series of customisable, flexible training courses designed to unlock new possibilities for your teams.

+

How Tarides Can Help You

+

Technical training equips your teams with essential skills to handle the latest software advancements and workflow improvements. While many generic courses exist, specialised knowledge is often necessary, and our targeted training suite offers:

+ +

Our bespoke training can be customised to the unique circumstances of each team, addressing weaknesses and enhancing strengths. Each course offers:

+ +

Sign up online for our courses, and we will contact you for an initial consultation to provide more information, discuss options, and help you decide if training is right for you!

+

Our Courses

+

We have created a group of courses tailored to different needs, ranging from onboarding a team with OCaml to mastering specialised skills, from basic compliance with cybersecurity guidelines to auditing custom workflows. While they address various applications, all of our training shares a common goal: to minimise friction for busy organisations. Our most popular courses are detailed below:

+

Getting Started With OCaml: An Introduction

+

Are you using OCaml for the first time or onboarding new team members? This course is a perfect fit. It covers the fundamental language concepts, tools, and techniques and culminates with a practical exercise in which participants build their own application. The course includes modules on the Dune build system, the OCaml Platform, imperative and modular programming, debugging, and more!

+

OCaml stands out among its peers with its expressive syntax, robust type system, and exceptional performance. After this course, your team will walk away with an understanding of OCaml's main features and how to start using them to their advantage.

+

Mastering OCaml: Advanced Techniques

+

This is the best choice for teams already familiar with OCaml and who are using it in their projects. It enables your teams to adopt advanced techniques, such as Web application development with JSOO and WSOO, multicore programming with Eio, MirageOS, testing, and GADTs, making expert-level techniques accessible to our clients.

+

This course allows you to customise modules to cover the exact tools and techniques your teams need the most. This allows them to improve the quality of the code they produce precisely and effectively, boosting OCaml developers’ confidence and skills.

+

Scalable, Flexible, and Powerful: Language-neutral Functional Programming

+

Help your teams understand the core functional programming principles that help developers produce safer, less buggy, and more readable code - regardless of their programming language. This three day course is a rich introduction to functional programming. The first day focusses on the foundations, including recursive and higher-order functions, type annotations and type inference, and function composition and pipes. The second day delves deeper into types covering topics like immutability, monads, and currying. The final day pushes further into I/O monads, continuations, type algebra, and more.

+

This course is the perfect choice for teams responding to the growing push for safer code, wanting to adopt functional programming in their workflows. It is also an excellent choice for onboarding new teams, helping them gain confidence and competence with a new way of programming.

+

Coming soon: More Courses and More Content!

+

Some of our training programmes are still under development. Register your interest in the upcoming courses to find out when they become available.

+ +

Get in Touch

+

We're excited to provide this service to our clients and know how important it is to share the knowledge we have accumulated. As the world increasingly recognises the need for change in how software is developed, OCaml, functional programming, and open source are growing. We are here to help you be ready for this transition!

+

Stay in touch with us on X, Mastodon, Threads, and LinkedIn. We look forward to hearing from you!

+ diff --git a/data/planet/watch-ocaml/ocaml23-buck2-for-ocaml-users--developers.md b/data/planet/watch-ocaml/ocaml23-buck2-for-ocaml-users--developers.md new file mode 100644 index 0000000000..91d946e23d --- /dev/null +++ b/data/planet/watch-ocaml/ocaml23-buck2-for-ocaml-users--developers.md @@ -0,0 +1,17 @@ +--- +title: '[OCaML''23] Buck2 for OCaml Users & Developers' +description: '[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 use...' +url: https://watch.ocaml.org/w/cYiKFa5EbS3AqVgYzMHP5V +date: 2024-09-29T15:48:58-00:00 +preview_image: https://watch.ocaml.org/lazy-static/previews/2b327168-249c-466f-a99b-bc1bde243dc7.jpg +authors: +- Watch OCaml +source: +--- + +

[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.

+ diff --git a/data/planet/watch-ocaml/ocaml23-building-a-lock-free-stm-for-ocaml.md b/data/planet/watch-ocaml/ocaml23-building-a-lock-free-stm-for-ocaml.md new file mode 100644 index 0000000000..bfb26f989c --- /dev/null +++ b/data/planet/watch-ocaml/ocaml23-building-a-lock-free-stm-for-ocaml.md @@ -0,0 +1,17 @@ +--- +title: '[OCaML''23] Building a lock-free STM for OCaml' +description: '[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...' +url: https://watch.ocaml.org/w/v3LtkXGeW5KXjziPQdzRJZ +date: 2024-09-29T15:39:28-00:00 +preview_image: https://watch.ocaml.org/lazy-static/previews/38e8d543-9ec5-4354-9e04-985d09d22571.jpg +authors: +- Watch OCaml +source: +--- + +

[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.

+ diff --git a/data/planet/watch-ocaml/ocaml23-efficient-ocaml-compilation-with-flambda-2.md b/data/planet/watch-ocaml/ocaml23-efficient-ocaml-compilation-with-flambda-2.md new file mode 100644 index 0000000000..3487bf1160 --- /dev/null +++ b/data/planet/watch-ocaml/ocaml23-efficient-ocaml-compilation-with-flambda-2.md @@ -0,0 +1,17 @@ +--- +title: '[OCaML''23] Efficient OCaml compilation with Flambda 2' +description: '[OCaML''23] Efficient OCaml compilation with Flambda 2 Pierre Chambart, + Vincent LAVIRON, Mark Shinwell Flambda 2 is an IR and optimisation pass for OCaml + centred around inlining. We discuss the engi...' +url: https://watch.ocaml.org/w/qGN45zFDCVGxiKRz9mKkVp +date: 2024-09-29T16:01:22-00:00 +preview_image: https://watch.ocaml.org/lazy-static/previews/54d5501a-b6ae-4106-bbdc-dbd09ab7da33.jpg +authors: +- Watch OCaml +source: +--- + +

[OCaML'23] Efficient OCaml compilation with Flambda 2

+

Pierre Chambart, Vincent LAVIRON, Mark Shinwell

+

Flambda 2 is an IR and optimisation pass for OCaml centred around inlining. We discuss the engineering constraints that shaped it and the overall structure that allows the compiler to be fast enough to handle very large industrial code bases.

+ diff --git a/data/planet/watch-ocaml/ocaml23-eio-10--effects-based-io-for-ocaml-5.md b/data/planet/watch-ocaml/ocaml23-eio-10--effects-based-io-for-ocaml-5.md new file mode 100644 index 0000000000..143547664b --- /dev/null +++ b/data/planet/watch-ocaml/ocaml23-eio-10--effects-based-io-for-ocaml-5.md @@ -0,0 +1,17 @@ +--- +title: "[OCaML'23] Eio 1.0 \u2013 Effects-based IO for OCaml 5" +description: "[OCaML'23] Eio 1.0 \u2013 Effects-based IO for OCaml 5 Thomas Leonard, + Patrick Ferris, Christiano Haesbaert, Lucas Pluvinage, Vesa Karvonen, Sudha Parimala, + KC Sivaramakrishnan, Vincent Balat, Anil Madh..." +url: https://watch.ocaml.org/w/9Hxc81ac3k6GQF1fdZLx7d +date: 2024-09-29T16:13:37-00:00 +preview_image: https://watch.ocaml.org/lazy-static/previews/66c29989-c956-45aa-b582-84a311c086fc.jpg +authors: +- Watch OCaml +source: +--- + +

[OCaML'23] Eio 1.0 – Effects-based IO for OCaml 5

+

Thomas Leonard, Patrick Ferris, Christiano Haesbaert, Lucas Pluvinage, Vesa Karvonen, Sudha Parimala, KC Sivaramakrishnan, Vincent Balat, Anil Madhavapeddy

+

Eio provides an effects-based direct-style IO stack for OCaml 5. This talk introduces Eio’s main features, such as use of effects, multi-core support and lock-free data-structures, support for modular programming, interoperability with other concurrency libraries such as Lwt, Async and Domainslib, and interactive monitoring support enabled by the custom runtime events in OCaml 5.1. We will report on our experiences porting existing applications to Eio.

+ diff --git a/data/planet/watch-ocaml/ocaml23-less-power-for-more-learning-restricting-ocaml-features-for-effective-teaching.md b/data/planet/watch-ocaml/ocaml23-less-power-for-more-learning-restricting-ocaml-features-for-effective-teaching.md new file mode 100644 index 0000000000..ea55750225 --- /dev/null +++ b/data/planet/watch-ocaml/ocaml23-less-power-for-more-learning-restricting-ocaml-features-for-effective-teaching.md @@ -0,0 +1,19 @@ +--- +title: '[OCaML''23] Less Power for More Learning: Restricting OCaml Features for Effective + Teaching' +description: '[OCaML''23] Less Power for More Learning: Restricting OCaml Features + for Effective Teaching Max Lang, Nico Petzendorfer We present a framework for sandboxing + and restricting features of the OCaml pr...' +url: https://watch.ocaml.org/w/uABzLbyAasoKbjyRwganh4 +date: 2024-09-29T16:04:22-00:00 +preview_image: https://watch.ocaml.org/lazy-static/previews/9915ec4a-8c53-46e5-b06d-61e1c91940b9.jpg +authors: +- Watch OCaml +source: +--- + +

[OCaML'23] Less Power for More Learning: Restricting OCaml Features for Effective Teaching

+

Max Lang, Nico Petzendorfer

+

We present a framework for sandboxing and restricting features of the OCaml programming language to effectively automate the grading of programming exercises, scaling to hundreds of submissions. We describe how to disable language and library features that should not be used to solve a given exercise. We present an overview of an implementation of a mock IO system to allow testing of IO-related exercises in a controlled environment. Finally, we detail a number of security considerations to ensure submitted code remains sandboxed, allowing automatic grading to be trusted without manual verification. The source code of our implementation is publicly available [1].
+[1] As a git repository at https://github.com/just-max/less-power.

+ diff --git a/data/planet/watch-ocaml/ocaml23-metaocaml-theory-and-implementation.md b/data/planet/watch-ocaml/ocaml23-metaocaml-theory-and-implementation.md new file mode 100644 index 0000000000..46ebbdcfc4 --- /dev/null +++ b/data/planet/watch-ocaml/ocaml23-metaocaml-theory-and-implementation.md @@ -0,0 +1,17 @@ +--- +title: '[OCaML''23] MetaOCaml Theory and Implementation' +description: '[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-processi...' +url: https://watch.ocaml.org/w/rnQXcND8aaY9qUtikB9tSc +date: 2024-09-29T15:35:39-00:00 +preview_image: https://watch.ocaml.org/lazy-static/previews/6fb93c0e-5afe-4a67-a158-00f303af7e44.jpg +authors: +- Watch OCaml +source: +--- + +

[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.

+ diff --git a/data/planet/watch-ocaml/ocaml23-modern-dsl-compiler-architecture-in-ocaml-our-experience-with-catala.md b/data/planet/watch-ocaml/ocaml23-modern-dsl-compiler-architecture-in-ocaml-our-experience-with-catala.md new file mode 100644 index 0000000000..4765309069 --- /dev/null +++ b/data/planet/watch-ocaml/ocaml23-modern-dsl-compiler-architecture-in-ocaml-our-experience-with-catala.md @@ -0,0 +1,20 @@ +--- +title: '[OCaML''23] Modern DSL compiler architecture in OCaml our experience with + Catala' +description: '[OCaML''23] Modern DSL compiler architecture in OCaml our experience + with Catala Louis Gesbert, Denis Merigoux In this presentation, we intend to show + a state-of-the-art DSL implementation in OCaml,...' +url: https://watch.ocaml.org/w/7ZxKnBY2w3XCztpzbKm8YG +date: 2024-09-29T16:16:23-00:00 +preview_image: https://watch.ocaml.org/lazy-static/previews/7584602b-9668-4289-bb86-e9721e157f8b.jpg +authors: +- Watch OCaml +source: +--- + +

[OCaML'23] Modern DSL compiler architecture in OCaml our experience with Catala

+

Louis Gesbert, Denis Merigoux

+

In this presentation, we intend to show a state-of-the-art DSL implementation in OCaml, with concrete examples and experience reports.
+In particular, we found that some advanced practices, while accepted among the hardcore OCaml developers (e.g. use of row type variables through object types), lacked visibility and documentation: some of them deserve to be better known.
+Our experience is based on the Catala compiler, a DSL for the implementation of algorithms defined in law.

+ diff --git a/data/planet/watch-ocaml/ocaml23-osiris-an-iris-based-program-logic-for-ocaml.md b/data/planet/watch-ocaml/ocaml23-osiris-an-iris-based-program-logic-for-ocaml.md new file mode 100644 index 0000000000..645fd885f4 --- /dev/null +++ b/data/planet/watch-ocaml/ocaml23-osiris-an-iris-based-program-logic-for-ocaml.md @@ -0,0 +1,17 @@ +--- +title: '[OCaML''23] Osiris: an Iris-based program logic for OCaml' +description: "[OCaML'23] Osiris: an Iris-based program logic for OCaml Arnaud Daby-Seesaram, + Fran\xE7ois Pottier, Arma\xEBl Gu\xE9neau Osiris is a project that aims to help + OCaml developers verify their code using Separa..." +url: https://watch.ocaml.org/w/1Hfi9pjTo1hz1ej2WtVGCR +date: 2024-09-29T15:27:45-00:00 +preview_image: https://watch.ocaml.org/lazy-static/previews/01208c4e-6774-4946-9ff6-69e0375dc3c2.jpg +authors: +- Watch OCaml +source: +--- + +

[OCaML'23] Osiris: an Iris-based program logic for OCaml

+

Arnaud Daby-Seesaram, François Pottier, Armaël Guéneau

+

Osiris is a project that aims to help OCaml developers verify their code using Separation Logic. The project is still young: we currently only support a subset of the features of the OCaml language, including modules, mutual recursion, ADTs, tuples and records. Ultimately, we would like to extend Osiris to support most features of the OCaml language. Iris is a Coq framework for Separation Logic with support for expressive ghost states. It is often used to define program logics and can be parameterized by a programming language — usually described by its small-steps semantics. Most Iris instantiations target ML-like languages, each focusing on a specific purpose and lacking support of programming features such as records or ADTs. Osiris contains an Iris instantiation with a presentation of the semantics of OCaml, in order to reason on realistic OCaml programs. Osiris provides a translation tool to convert OCaml files to Coq files (cf. section 2). In order to verify an OCaml program with Osiris, one would use the translator on an OCaml file, seen as a module. This produces a Coq file containing a deep-embedded representation me of the module. The user would then write and prove a specification for the interpretation of me in our semantics.

+ diff --git a/data/planet/watch-ocaml/ocaml23-owi-an-interpreter-and-a-toolkit-for-webassembly-written-in-ocaml.md b/data/planet/watch-ocaml/ocaml23-owi-an-interpreter-and-a-toolkit-for-webassembly-written-in-ocaml.md new file mode 100644 index 0000000000..5eeaa5ab09 --- /dev/null +++ b/data/planet/watch-ocaml/ocaml23-owi-an-interpreter-and-a-toolkit-for-webassembly-written-in-ocaml.md @@ -0,0 +1,17 @@ +--- +title: '[OCaML''23] Owi: an interpreter and a toolkit for WebAssembly written in OCaml' +description: "[OCaML'23] Owi: an interpreter and a toolkit for WebAssembly written + in OCaml L\xE9o Andr\xE8s, Pierre Chambart, Eric Patrizio, Dario Pinto This presentation + introduces Owi, an OCaml-based interpreter an..." +url: https://watch.ocaml.org/w/3pYGmveWpNNLH4B6TUv5ww +date: 2024-09-29T15:25:04-00:00 +preview_image: https://watch.ocaml.org/lazy-static/previews/da695cb1-3459-48bc-949b-ab4b84263c1e.jpg +authors: +- Watch OCaml +source: +--- + +

[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.

+ diff --git a/data/planet/watch-ocaml/ocaml23-parallel-sequences-in-multicore-ocaml.md b/data/planet/watch-ocaml/ocaml23-parallel-sequences-in-multicore-ocaml.md new file mode 100644 index 0000000000..6508c913bc --- /dev/null +++ b/data/planet/watch-ocaml/ocaml23-parallel-sequences-in-multicore-ocaml.md @@ -0,0 +1,17 @@ +--- +title: '[OCaML''23] Parallel Sequences in Multicore OCaml' +description: '[OCaML''23] Parallel Sequences in Multicore OCaml Andrew Tao I present + my implementation of a parallel sequences abstraction that utilizes the support + for shared memory parallelism in the new OCaml ...' +url: https://watch.ocaml.org/w/6K7mqY88PyDZFC2bJvs2Xe +date: 2024-09-29T15:40:29-00:00 +preview_image: https://watch.ocaml.org/lazy-static/previews/fe7678aa-6348-45bd-b293-caf5f8877e35.jpg +authors: +- Watch OCaml +source: +--- + +

[OCaML'23] Parallel Sequences in Multicore OCaml

+

Andrew Tao

+

I present my implementation of a parallel sequences abstraction that utilizes the support for shared memory parallelism in the new OCaml 5.0.0 multicore runtime. This abstraction allows clients to create highly parallelizable programs without needing to write, or even understand, the low-level implementation details necessary to parallelize large tasks.

+ diff --git a/data/planet/watch-ocaml/ocaml23-state-of-the-ocaml-platform-2023.md b/data/planet/watch-ocaml/ocaml23-state-of-the-ocaml-platform-2023.md new file mode 100644 index 0000000000..bca0c19101 --- /dev/null +++ b/data/planet/watch-ocaml/ocaml23-state-of-the-ocaml-platform-2023.md @@ -0,0 +1,18 @@ +--- +title: '[OCaML''23] State of the OCaml Platform 2023' +description: '[OCaML''23] State of the OCaml Platform 2023 Thibaut Mattio, Anil Madhavapeddy, + Thomas Gazagnaire, David Allsopp This paper reflects on a decade of progress and + developments within the OCaml Platfor...' +url: https://watch.ocaml.org/w/9GtFUSDDpmU8ZDD54A7V7e +date: 2024-09-29T15:27:19-00:00 +preview_image: https://watch.ocaml.org/lazy-static/previews/96763544-5622-470d-8ef0-bdd191d657e7.jpg +authors: +- Watch OCaml +source: +--- + +

[OCaML'23] State of the OCaml Platform 2023

+

Thibaut Mattio, Anil Madhavapeddy, Thomas Gazagnaire, David Allsopp

+

This paper reflects on a decade of progress and developments within the OCaml Platform, from its inception in 2013 with the release of opam 1.0, to today where it stands as a robust toolchain for OCaml developers. We review the last three years in detail, emphasizing the advancements and innovations that have shaped the OCaml development landscape and highlighting key milestones such as the migration to Dune as the primary build system, and the development of a Language Server Protocol (LSP) server for OCaml.
+We also outline our plan for the coming years. The roadmap is informed by community feedback, discussions with Platform tool maintainers, and insights from industrial users of OCaml. The final version of this evolving roadmap, designed to shape the future of the OCaml developer experience, will be presented at the International Conference on Functional Programming (ICFP).

+ diff --git a/data/planet/watch-ocaml/ocaml23-targeted-static-analysis-for-ocaml-c-stubs-eliminating-gremlins-from-the-code.md b/data/planet/watch-ocaml/ocaml23-targeted-static-analysis-for-ocaml-c-stubs-eliminating-gremlins-from-the-code.md new file mode 100644 index 0000000000..67fb39644b --- /dev/null +++ b/data/planet/watch-ocaml/ocaml23-targeted-static-analysis-for-ocaml-c-stubs-eliminating-gremlins-from-the-code.md @@ -0,0 +1,20 @@ +--- +title: '[OCaML''23] Targeted Static Analysis for OCaml C Stubs: Eliminating gremlins + from the code' +description: "[OCaML'23] Targeted Static Analysis for OCaml C Stubs: Eliminating gremlins + from the code Edwin T\xF6r\xF6k Migration to OCaml 5 requires updating a lot of + C bindings due to the removal of naked pointer ..." +url: https://watch.ocaml.org/w/sj5jf9iieZA7E1cbDbnv2j +date: 2024-09-29T14:32:44-00:00 +preview_image: https://watch.ocaml.org/lazy-static/previews/02fc8f1e-7e60-4f76-af5f-8228533fb06f.jpg +authors: +- Watch OCaml +source: +--- + +

[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.

+ diff --git a/data/planet/watch-ocaml/outreachy-may-2024-demo.md b/data/planet/watch-ocaml/outreachy-may-2024-demo.md new file mode 100644 index 0000000000..7aa6d3f787 --- /dev/null +++ b/data/planet/watch-ocaml/outreachy-may-2024-demo.md @@ -0,0 +1,16 @@ +--- +title: Outreachy May 2024 Demo +description: The OCaml community participated in the May 2024 round of Outreachy internships. + Three interns worked on a range of projects including tools to diff OCaml APIs, + more accessible diffing tools and ru... +url: https://watch.ocaml.org/w/peT3MdWjS1BYYMbowEJ1gv +date: 2024-09-07T15:07:21-00:00 +preview_image: https://watch.ocaml.org/lazy-static/previews/1a1f5808-073c-4970-86cb-f60729386693.jpg +authors: +- Watch OCaml +source: +--- + +

The OCaml community participated in the May 2024 round of Outreachy internships. Three interns worked on a range of projects including tools to diff OCaml APIs, more accessible diffing tools and running OCaml exercises anywhere!

+

This meeting was an opportunity for the interns to present their work and for the community to ask questions and was originally announced on the discuss forum.

+ diff --git a/data/watch.yml b/data/watch.yml index 250f60407d..863841bc68 100644 --- a/data/watch.yml +++ b/data/watch.yml @@ -832,6 +832,15 @@ watch: published_at: 2015-09-18T00:00:00.000Z language: English category: Science & Technology +- name: Outreachy May 2024 Demo + description: The OCaml community participated in the May 2024 round of [Outreachy](https://www.outreachy.org/) + internships. Three interns worked on a range of projects including tools to diff + OCaml APIs, more accessible diffing tools and running OCaml exercise... + embed_path: /videos/embed/bc32514d-b431-4cb1-80b7-e7d11d130eb3 + thumbnail_path: /lazy-static/thumbnails/1d2a2bf4-5494-4c96-9227-0c6d663288e8.jpg + published_at: 2024-09-07T15:07:21.999Z + language: English + category: Science & Technology - name: Outreachy Presentations for the December 2021 Round description: The OCaml community participated in the December 2021 round of [Outreachy](https://www.outreachy.org/) internships. Three interns worked on a range of projects including OCaml's pre-processor @@ -1341,6 +1350,167 @@ watch: published_at: 2018-11-26T00:00:00.000Z language: English category: Science & Technology +- name: '[OCaML''23] Buck2 for OCaml Users & Developers' + description: '[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 al...' + embed_path: /videos/embed/60f11df8-14ed-489a-a85a-457659f3e911 + thumbnail_path: /lazy-static/thumbnails/86b07f08-f89c-4c92-a268-c3b352e6fb63.jpg + published_at: 2023-12-01T00:00:00.000Z + language: English + category: Science & Technology +- name: '[OCaML''23] Building a lock-free STM for OCaml' + description: '[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-fr...' + embed_path: /videos/embed/eb3bea49-8fe0-441b-a4fc-3f36e478d8c9 + thumbnail_path: /lazy-static/thumbnails/b1112b17-a84a-45d5-80b7-d7dbba4a18f8.jpg + published_at: 2023-12-01T00:00:00.000Z + language: English + category: Science & Technology +- name: '[OCaML''23] Efficient OCaml compilation with Flambda 2' + description: '[OCaML''23] Efficient OCaml compilation with Flambda 2 + + + Pierre Chambart, Vincent LAVIRON, Mark Shinwell + + + Flambda 2 is an IR and optimisation pass for OCaml centred around inlining. We + discuss the engineering constraints that shaped it and the overa...' + embed_path: /videos/embed/c80d75b9-88dd-42f4-9c11-c96b699e9e7d + thumbnail_path: /lazy-static/thumbnails/add0528c-59d2-4107-80d5-16a752a8d186.jpg + published_at: 2023-12-01T00:00:00.000Z + language: French + category: Science & Technology +- name: "[OCaML'23] Eio 1.0 \u2013 Effects-based IO for OCaml 5" + description: "[OCaML'23] Eio 1.0 \u2013 Effects-based IO for OCaml 5\n\nThomas Leonard, + Patrick Ferris, Christiano Haesbaert, Lucas Pluvinage, Vesa Karvonen, Sudha Parimala, + KC Sivaramakrishnan, Vincent Balat, Anil Madhavapeddy\n\nEio provides an effects-based + direct-st..." + embed_path: /videos/embed/4695d391-9e90-4b54-b6c9-407fa1ed3a34 + thumbnail_path: /lazy-static/thumbnails/bcc3f2e9-bae2-4cdf-a5b3-ac5408ab6a95.jpg + published_at: 2023-12-01T00:00:00.000Z + language: English + category: Science & Technology +- name: '[OCaML''23] Less Power for More Learning: Restricting OCaml Features for + Effective Teaching' + description: '[OCaML''23] Less Power for More Learning: Restricting OCaml Features + for Effective Teaching + + + Max Lang, Nico Petzendorfer + + + We present a framework for sandboxing and restricting features of the OCaml programming + language to effectively automate the g...' + embed_path: /videos/embed/e7951952-00d7-4346-aaa3-b4773397c3ef + thumbnail_path: /lazy-static/thumbnails/15f092e5-7a77-42e8-843b-8567c22ade38.jpg + published_at: 2023-12-01T00:00:00.000Z + language: English + category: Science & Technology +- name: '[OCaML''23] MetaOCaml Theory and Implementation' + description: '[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....' + embed_path: /videos/embed/cd8140d6-e474-4076-bf94-2d9c55f8dd3b + thumbnail_path: /lazy-static/thumbnails/46603480-ba59-4b26-afaf-4c9b47cbffcd.jpg + published_at: 2023-12-01T00:00:00.000Z + language: English + category: Science & Technology +- name: '[OCaML''23] Modern DSL compiler architecture in OCaml our experience with + Catala' + description: '[OCaML''23] Modern DSL compiler architecture in OCaml our experience + with Catala + + + Louis Gesbert, Denis Merigoux + + + In this presentation, we intend to show a state-of-the-art DSL implementation + in OCaml, with concrete examples and experience reports. ...' + embed_path: /videos/embed/389fcac9-135f-4b6e-9afd-6215ddecdaa4 + thumbnail_path: /lazy-static/thumbnails/dc4c7f91-9ea8-4901-b51a-a33d6cc6aa88.jpg + published_at: 2023-12-01T00:00:00.000Z + language: English + category: Science & Technology +- name: '[OCaML''23] Osiris: an Iris-based program logic for OCaml' + description: "[OCaML'23] Osiris: an Iris-based program logic for OCaml\n\nArnaud + Daby-Seesaram, Fran\xE7ois Pottier, Arma\xEBl Gu\xE9neau\n\nOsiris is a project + that aims to help OCaml developers verify their code using Separation Logic. The + project is still young: we curre..." + embed_path: /videos/embed/05c24df6-ce44-4571-ab46-43970f44e4f1 + thumbnail_path: /lazy-static/thumbnails/23651eeb-a9d4-41ee-a39d-54e9037581b5.jpg + published_at: 2023-12-01T00:00:00.000Z + language: English + category: Science & Technology +- name: '[OCaML''23] Owi: an interpreter and a toolkit for WebAssembly written in + OCaml' + description: "[OCaML'23] Owi: an interpreter and a toolkit for WebAssembly written + in OCaml\n\nL\xE9o Andr\xE8s, Pierre Chambart, Eric Patrizio, Dario Pinto\n\nThis + presentation introduces Owi, an OCaml-based interpreter and toolkit for WebAssembly + (Wasm). Owi aims to pr..." + embed_path: /videos/embed/138b52f3-7867-4a37-9b9a-81d08c3983e2 + thumbnail_path: /lazy-static/thumbnails/372aa447-5e78-4748-8486-7eaf2f36a5f0.jpg + published_at: 2023-12-01T00:00:00.000Z + language: French + category: Science & Technology +- name: '[OCaML''23] Parallel Sequences in Multicore OCaml' + description: '[OCaML''23] Parallel Sequences in Multicore OCaml + + + Andrew Tao + + + I present my implementation of a parallel sequences abstraction that utilizes + the support for shared memory parallelism in the new OCaml 5.0.0 multicore runtime. + This abstraction allows...' + embed_path: /videos/embed/2e829712-4a69-465f-a8e7-94f102e737c7 + thumbnail_path: /lazy-static/thumbnails/872f631d-7b82-4700-aafd-51984c131dfd.jpg + published_at: 2023-12-01T00:00:00.000Z + language: English + category: Science & Technology +- name: '[OCaML''23] State of the OCaml Platform 2023' + description: '[OCaML''23] State of the OCaml Platform 2023 + + + Thibaut Mattio, Anil Madhavapeddy, Thomas Gazagnaire, David Allsopp + + + This paper reflects on a decade of progress and developments within the OCaml + Platform, from its inception in 2013 with the release o...' + embed_path: /videos/embed/466fec6a-4ce5-451f-8cdc-859916d8dc4d + thumbnail_path: /lazy-static/thumbnails/3b6c229d-0671-4e60-aeee-8843e914c56e.jpg + published_at: 2023-12-01T00:00:00.000Z + language: English + category: Science & Technology +- name: '[OCaML''23] Targeted Static Analysis for OCaml C Stubs: Eliminating gremlins + from the code' + description: "[OCaML'23] Targeted Static Analysis for OCaml C Stubs: Eliminating + gremlins from the code\n\nEdwin T\xF6r\xF6k\n\nMigration to OCaml 5 requires updating + a lot of C bindings due to the removal of naked pointer support. Writing OCaml + user-defined primitives i..." + embed_path: /videos/embed/d513a6e6-86c6-4202-9431-d3479ff60b68 + thumbnail_path: /lazy-static/thumbnails/c5717695-9ee2-4553-afff-78c5aed46aa7.jpg + published_at: 2023-12-01T00:00:00.000Z + language: English + category: Science & Technology - name: gloc - Metaprogramming WebGL Shaders with OCaml description: "\r\ngloc : Metaprogramming WebGL Shaders with OCaml, by David William Wallace Sheets and Ashima Arts.\r\n\r\nWebGL is a new Khronos Group standard for