[Experimental] Quasi-static scheduler

[lsk567]

This PR implements a quasi-static (QS) scheduler proposed in #1080. The QS scheduler generates a fixed static schedule at compile time and follows the fixed schedule at runtime.

To use this scheduler, the user needs to install two additional dependencies: Uclid5 and z3. Both need to be added to PATH and able to be invoked on the command line.

The scheduler is currently experimental (i.e. not production-ready). For small test cases such as ThreadedThreaded.lf, it can achieve comparable performance wrt that of the default NP scheduler. However, for large benchmarks such as SleepingBarber.lf, the QS scheduler currently exhibits a significant slowdown. We are yet to figure out the cause of this.

[lsk567]

Please note that unless this eventually gets merged with a squash commit, these papers will continue to linger in Git's history. Perhaps now is the time to create a new branch (forked off master) and quash your changes in this branch into the new one (using a PR). You can then continue developing in that new branch and eventually submit a clean PR to master.

@lhstrh Okay, sounds good to me.

[lsk567]

@Soroosh129 brought up the issue that naming the implementation a "quasi-static scheduler" might be too generic, since there can be different variants of the quasi-static scheduler (e.g. a QS scheduler with a schedule generation mechanism using some other constraint solvers). When specifying the QS scheduler, it would be useful to further parametrize the scheduler. For example, scheduler: QS(smt).

[lhstrh]

When specifying the QS scheduler, it would be useful to further parametrize the scheduler. For example, scheduler: QS(smt).

This strikes me as excess generality. Wouldn't something like qs-uclid5 do?