search

HeisenbugLtd / spat

SPARK Proof Analysis Tool
https://github.heisenbug.eu/spat/
Do What The F*ck You Want To Public License
15 stars 4 forks source link

Sorting is not deterministic #18

Closed Jellix closed 4 years ago

Jellix commented 4 years ago

See below for the reoccurence

The fix for issue #13 revealed that sorting is not stable.

In case of sorting by time, when two times are identical, we also need to take the entity name/source location into account, I'm afraid.

For VCs, the total_proof_time, the maximum_proof time and then the entity location should be compared.

It's a bit unclear what to do with single proof paths, though. They all reference the same location and entity, even sorting by prover name could result in undeterministic behaviour.

Jellix commented 4 years ago

I tried adding steps to the sorting criteria, now the templates fail again.

Although unlikely, I am suspecting some floating point to fixed point conversion issues.

See fix_sorting branch which currently fails templates and the differences should not actually be there, unless the time values are actually different.

Jellix commented 4 years ago

I think I found the issue. It's not the sorting between the proof attempts, but between the proof items. They don't know about steps, and the offending entries have all the same value (max time, total time, rule, severity, and location), so unstable sorting is to be expected. I guess, to stabilize that we need to create unique ids to make these guys different, assuming that (at least for the tests) we can guarantee the order in which the entries are inserted.

Jellix commented 4 years ago

Fixed in #28