Deterministic Builds

[DavePearce]

For reasons unknown (though probably connected with Rayon), corset builds are currently non-deterministic. That is, generating the same bin file twice leads to different output. This makes it very hard indeed to track changes between builds, and needs to be resolved ASAP.

This issue manifests itself in two ways:

• (File Size) the resulting files have different sizes.

• (Constraint Ordering) the resulting constraints have different orderings. For example, in the generated go file we can sometimes get this:

  add := Interleave(add_H, add__BYTE_1, add__BYTE_2)

  whilst other times we get this:

  add := Interleave(add_H, add__BYTE_2, add__BYTE_1)

  Its unclear to me whether these are equivalent.

[DavePearce]

Note running with corset -t 1 ... does not resolve this issue. It also could mean that, in order to safely generate the bin and go files they need to be done at the same time?

[delehef]

It also could mean that, in order to safely generate the bin and go files they need to be done at the same time?

It's probably stemming from the fact that HashMap iteration is not guaranteed to be reproducible; BTreeMap e.g. is.

[DavePearce]

Yeah, that is one of the normal reasons for non-determinism. I guess the question is whether or not the difference in the output above actually matters?

[DavePearce]

UPDATE: Something very unexpected is going on here. Given this input file: permute.lisp

(module test)
(defcolumns A)
(defpermutation (B) ((+ A)))
(defconstraint test () (vanishes! (+ A B)))

permute.trace

{"test": { "A": [1] } }

Then, I had this session:

$ corset convert --format csv --trace permute.trace permute.lisp
$ cat trace.csv_test 
A,B
0,0x1
$ corset convert --format csv --trace permute.trace permute.lisp
$ cat trace.csv_test 
A,B
0x1,0

Notice how the ordering can change between consecutive runs. Surely that cannot make sense, right?