Better resolution of violations between runs. #28
Description
Currently, sequential runs of ECSTATIC must recompute violations. I originally had a feature that would pickle violations and then, if there were pickled violations available, read those instead of recomputing. However, I ran into various issues with this.
- How to know whether the violations are up-to-date and complete? What if somebody killed the previous run of ECSTATIC midway through writing violations, or recomputed some analysis result?
- How to store the violations in a non-redundant way? .pickle files are not human readable, but the .json files we use as the human-readable format do not (and cannot) have all the information we need to read violations back in to a usable format.
Some potential ideas I've had:
- Have some sentinel file we write after processing is done, including a hash of the result files and/or violations. If this sentinel file is inconsistent with the runtime hash, we recompute violations.
- Use a database instead of files for output. This would probably make everybody's life easier, because frankly, the file-based results structure can be a pain in the ass. I originally wrote it this way to allow easy command-line processing (e.g., being able to count partial order bugs, violations), but it is unwieldy and huge.