septract / starling-tool

An automatic verifier for concurrent algorithms.
MIT License
7 stars 4 forks source link

Decouple pipeline #144

Open MattWindsor91 opened 7 years ago

MattWindsor91 commented 7 years ago

I'm working on some proposals to make Starling more interactive (eg. guided inference of view expressions, #143) and reactive (eg. using inference at the end of the pipeline then re-evaluating proof cycles).

I think what would be useful is if we refactored Starling from a strict pipeline to a more dependency-based approach where, for example, all of the various stages of a Starling proof generation are stored together as options in a big Proof object, and then the pipeline stages correspond to asking for a specific part of that object and back-propagating requests for earlier stages to calculate it.

That way, reactive processes can just replace the newly inferred bits of the Starling proof and rerun the later stages, and interactive processes can more easily selectively run off smaller bits of the Starling proof process to test possible solutions.

MattWindsor91 commented 7 years ago

This seems like it's something that could take a while to crunch through and become a massive rabbit hole, but I'm not sure how else to structure Starling for inference without making the pipeline an unholy mess.

Feels like playing around with this should be a weekend project to start with maybe.

@BenSimner I vaguely remember you suggesting something like this (though it might have been specifically for bits of proof rather than the whole context) and at the time I was wary of doing so. Thoughts?