Use Stdlib instead of deprecated Pervasives for 5.00.0+trunk

[shakthimaan]

The Pervasives module has been deprecated in OCaml 5.00.0+trunk, and the recommendation is to use the Stdlib module instead.

[kit-ty-kate]

What is the reasoning behind this? Using Obj.magic below seems highly dangerous

[kit-ty-kate]

Did the compiler tell you there was no use of Stdlib here? If not removing an open is dangerous as it shadows comparision functions such as compare that might be used somewhere

[kit-ty-kate]

Same question here

[mattiasdrp]

Hi, thanks for this PR. Could you split your commits in two, one for the Pervasives -> Stdlib and one for the redefinition of State with Obj and provide some explanation as to why this change?

[kit-ty-kate]

@mattiasdrp done in #6

[lthls]

A warning about this PR: I wrote this code a few months ago to allow cubicle to compile with Flambda 2 (except for the Pervasives -> Stdlib parts). I think it's not in a mergeable state right now: there's an Obj.magic call remaining, and the hash function will always return 0 for any state.

The main idea for the State module is to use from the start a representation of states that the GC doesn't need to scan. There are various other alternatives (some that don't even use Obj), but the complexity and impact on performance can vary.
I think that if letting the GC scan the state array is not too much of a problem, you should just merge #6 and forget this.
If you want to keep the same performance and be compatible with 5.0, then I would suggest discussing the options before making any decision.

[gasche]

I ended up by clicking at stuff randomly. Apologies!

Two comments:

• It is surprising to learn that a tricky part of a commit by @shakthimaan was in fact written by @lthls months ago. I would recommend using at least Co-authored-by: metadata, and preferably splitting commits to keep the original authors of well-identified changes.
• If I understand correctly, Cubicle heavily relies on its "state" type (it's a model checker so there are lots of states :-) implemented as int array, and it is using an ugly set_tag hack to mark the arrays with Obj.no_scan_tag to avoid having the GC waste time traversing all states. A proposal: could states be represented using Bytes instead, using the Bytes.get_int64_ne and Bytes.set_int64_ne primitives for accessing elements?

(Another idea is Bigarray, but it's unclear to me what the performance impact would be, whereas Bytes sound like they perform comparably to normal arrays.)

[lthls]

A proposal: could states be represented using Bytes instead, using the Bytes.get_int64_ne and Bytes.set_int64_ne primitives for accessing elements?

Pros: Efficient memory layout (only one more word compared to int arrays)
Cons: Needs conversions back and forth between Int64.t and int, slow accesses on non-x86 hardware

(Another idea is Bigarray, but it's unclear to me what the performance impact would be, whereas Bytes sound like they perform comparably to normal arrays.)

Pros: Support for int bigarrays available, reliable performance
Cons: Extra indirection for accesses compared to arrays

Both approaches also require patching the client code, which I was too lazy to do in my PR (but that shouldn't be a problem when implementing a robust solution).

[gasche]

Needs conversions back and forth between Int64.t and int.

let get arr i = Int64.to_int (Bytes.get_int64_ne arr (i*8))

$ ocamlopt -dcmm -c test.ml
[...]
(function{test.ml:1,8-59} camlTest__get_81 (arr/83: val i/84: val)
 (+
   (<<
     (let (prim/224 (+ (<< i/84 3) -7)
           index/225 (>>s prim/224 1))
       (checkbound [...])
       (load_mut int (+ arr/83 index/225)))
     1)
   1))

It looks like the compiler removes the coercions here. (I had checked before making the suggestion.)

[lthls]

It looks like the compiler removes the coercions here. (I had checked before making the suggestion.)

You'll notice that little (+ (<< (...) 1) 1) remaining. It's not a big deal, but you don't get that with int array.

[gasche]

Ah, right. Meh.

[lthls]

To be honest, the problem is that the coercions are only removed with the native code compiler for a 64-bit x86 backend. Try the same code with the bytecode compiler, or on a 32-bit architecture, or on a 64-bit Mac M1, and you'll get different code.

[gasche]

I don't know if anyone runs model checkers on 32bit architectures anymore. Regarding arm64, I think that the situation could be improved in this case, are we are indexing with obviously-aligned indices (i*8). This being said, this was a suggestion in passing, for a solution somewhere nice in the axis between safety and performance. (I'm also a bit worried about the verbosity of bound checks with String/Bytes.) I suspect that your solution using Obj.with_tag is actually reasonable, in line with the ugly hack the code was previously using. One could use Custom instead of Abstract if hashing proved to be an issue.

[lthls]

I don't know if anyone runs model checkers on 32bit architectures anymore.

Wait until people compile their model checkers to WebAssembly and run them in their browsers :)

One could use Custom instead of Abstract if hashing proved to be an issue.

Using a Custom tag implies writing a C stub (even the Obj API doesn't allow you to create well-formed custom blocks); if we're fine with that it's a decent solution. Redefining the hash function manually isn't that complicated either.