xs-opam icon indicating copy to clipboard operation
xs-opam copied to clipboard

Add tools and atomic datastructures to upstream-extra

Open edwintorok opened this issue 1 year ago • 4 comments

Add some useful tools (that I had pinned in my local opam switch for a while):

  • ocaml-print-intf: is useful for creating .mli files in a dune project (or at least a starting point for one)
  • opam-dune-lint: can find some missing dependencies in opam files that are present in dune files (not all ... yet)

Also add some parallelism-safe data structures that work on both OCaml 4 and OCaml 5:

  • saturn and saturn-lockfree contains very efficient, domain and thread-safe imperative data structures. It is well tested, and the algorithms are quite well known and used in other languages (property testing and fuzzing with qcheck, and qcheck-stm; model checking with dscheck, and some in-progress formal proofs)

  • kcas and kcas_data which provide composable lock-free data structures. Where composability is not needed saturn is likely faster and uses less memory, but where composability or transactions are needed this is more flexible. This could be useful for XAPI's main database (if we thread through the 'Xt' transaction log). The algorithms are similar to optimistic concurrency control: try to perform all operations assuming you'd succeed, and keep track of which values you've read inside a transaction, and then commit or rollback and restart depending on whether any of those values have changed; and is quite similar to how the transactions work in oxenstored. This allows for transactions that don't interfere with each-other to proceed in parallel. Some attention to detail is still needed, as this doesn't eliminate all concurrency bugs (read skew and write skew are still possible, but there are mechanisms for avoiding them, see the tutorial in the https://github.com/ocaml-multicore/kcas?tab=readme-ov-file#beware-of-torn-reads)

Adding these tools and libraries should be safe, as nothing in the product would use them yet. And we can gradually introduce them into XAPI behind a feature flag, only switching to them when we are confident that they work well for our use case.

We also gain some testing tools that are generally useful for XAPI (I've used some of these in various branches already):

  • qcheck-stm: for checking that a module matches a reference implementation (this is what found some of those security bugs in oxenstored)

Some other useful libraries that get brought in as dependencies:

  • thread-table: this is a magic-free thread-local-storage implementation for OCaml 4, and can be used to optimize our named mutex handling in XAPI (one of my branches will depend on something similar that was hand-written, but probably better to use this one instead). Not Domain-safe for OCaml 5, so we'll have to figure another solution for that, maybe by that time the standard library will have something (there is a 'thread-local-storage' on opam, but it relies on Obj.magic)

These libraries also bring in multicore-magic, which sounds .. dangerous ... although from its description perhaps most of this will get integrated into future OCaml 5 releases. With careful use of kcas and saturn we might be able to avoid most of the unsafe operations though (they are mostly meant as internal performance optimizations), although I'm still somewhat worried about its presence in the dependencies. We'll need to reevaluate this when we have some actual code that uses kcas/ saturn though.

edwintorok avatar Sep 19 '24 17:09 edwintorok

Have we moved to collect the libraries that we package into an RPM based on dependencies? Previously packaging was based on the tree hierarchy. @psafont

lindig avatar Sep 20 '24 08:09 lindig

We can't move to a dependency-bases system yet until all the issues surrounding tarball generation andpackage retrieval from it are fixed in opam. They are fixed in master, and should be available in the next major version (2.3.0, 2025.2, ???) The branch with the dependency-based system is present at https://github.com/xapi-project/xs-opam/compare/master...psafont:xs-opam:reorg

psafont avatar Sep 20 '24 10:09 psafont

I'm not too happy with the amount of dependencies being added here, we should do some trimming beforehand. For example goblint pulls a lot of dependencies. And while it's packages, it's still unused

psafont avatar Sep 20 '24 10:09 psafont

And while it's packages, it's still unused

I'll try to find some time on the next OIL day to update the analyzer so we can start using it with XAPI. You are right it has now been more than a year since I originally wrote the analyzer and I haven't been able to find the time to finish the CI integration. Unfortunately dune doesn't support pattern rules (like Makefiles) do, and I started writing a dune generator https://github.com/edwintorok/lintcstubs/tree/genrules2, https://github.com/edwintorok/lintcstubs/compare/main...genrules2maybe, but I'm not happy with the outcome.

I think it'll be easier to do the parallelisation of the analysis inside the tool itself rather than generating dune (and relying on its caching).

Lets keep this PR open meanwhile (I'll likely need to update goblint to a newer version too).

edwintorok avatar Sep 23 '24 08:09 edwintorok

@edwintorok this PR looks stale and has conflicts. I think we should close it and reopen if you've got an updated version.

robhoes avatar Apr 03 '25 16:04 robhoes

Removed 2 bugfix commits, the one about ezxenstore is already fixed, the one about xapi-rrdd is no longer relevant because the package got deleted.

edwintorok avatar Apr 07 '25 16:04 edwintorok

I'll reopen when I have code that uses these (although somewhat chicken and egg, because not having these present makes using these libraries more difficult as it requires a forked xs-opam that has to be kept up-to-date with master).

edwintorok avatar Apr 07 '25 16:04 edwintorok