crytic/echidna

[Bug-Candidate]: Echidna is non-deterministic when workers > 1

ggrieco-tob opened this issue · 1 comments

Describe the issue:

Echidna provide different results even if the seed is fixed, when the amount of workers is more than one. I'm using json output to hash the result of the campaign and compare them. This issue is NOT caused by the possible non-deterministic serialization of json (I verified that the output values are actually different).

Code example to reproduce the issue:

Execute the following bash program from the echidna directory which will run `tests/solidity/basic/flags.sol:

while $(true); do echidna tests/solidity/basic/flags.sol --test-limit 10000 --shrink-limit 333 --format json --seed 123 --workers 8 | tail -n 1 | md5sum ; done```

Version:

echidna compiled from master (2711374).

Relevant log output:

$ while $(true); do echidna tests/solidity/basic/flags.sol --test-limit 10000 --shrink-limit 333 --format json --seed 123 --workers 8 | tail -n 1 | md5sum ; done
bdc6c808805e5d6eb6d5cf4c23469525  -
bdc6c808805e5d6eb6d5cf4c23469525  -
ead6b2624de00e59b41aba2caec7c82b  -
bdc6c808805e5d6eb6d5cf4c23469525  -
arcz commented

@ggrieco-tob We can't guarantee that the campaign is deterministic with multiple workers anymore. It will depend on thread scheduling which is out of control for us. Not sure if we can improve things here.