[Experimental] Quasi-static scheduler #1190

lsk567 · 2022-05-23T21:35:35Z

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.

Soroosh129 · 2022-05-23T21:53:51Z

org.lflang/src/org/lflang/generator/c/CCmakeGenerator.java


+        if (targetConfig.schedulerType == SchedulerOption.QS) {


I think it's better to handle this here with a

if (targetConfig.schedulerType == SchedulerOption.QS) { targetConfig.compileDefinitions.put("SCHEDULER_QS", ""); }

Great, thanks! This is indeed a cleaner approach.

Soroosh129 · 2022-05-23T21:55:08Z

org.lflang/src/org/lflang/generator/c/CCoreFilesUtils.java

+            "threaded/scheduler_" + scheduler + ".c",
+            "threaded/reactor_threaded.c"
+        ));
+        if (scheduler == SchedulerOption.QS)


This would also be better handled here.

Soroosh129 · 2022-05-23T21:56:50Z

org.lflang/src/org/lflang/generator/c/CGenerator.java

+            System.out.println(this.main);
+            System.out.println(main);
+
+            // Generate schedule.h if QS scheduler is used.


Sorry to repeat this, but this should also be in pickScheduler I think.

Makes sense. Will revise the code accordingly. Thanks.

Soroosh129 · 2022-05-23T21:57:50Z

org.lflang/src/org/lflang/generator/c/CTriggerObjectsGenerator.java

@@ -161,6 +166,13 @@ public static String generateInitializeTriggerObjects(
            isFederated,
            clockSyncIsOn
        ));
+        if (targetConfig.schedulerType == SchedulerOption.QS) {


Why not have this inside generateSchedulerInitializer?

Right, it makes sense to have this in generateSchedulerInitializer. Thanks for the catch!

lsk567 · 2022-05-24T21:34:01Z

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.

lhstrh · 2022-05-24T21:36:53Z

build.gradle

@@ -33,6 +33,9 @@ subprojects {
        implementation group: 'com.google.inject', name: 'guice', version: guiceVersion
        // https://mvnrepository.com/artifact/commons-cli/commons-cli
        implementation group: 'commons-cli', name: 'commons-cli', version: commonsCliVersion
+        // https://search.maven.org/artifact/tools.aqua/z3-turnkey/4.8.16/jar
+        implementation 'tools.aqua:z3-turnkey:4.8.16'


I noticed that this added dependency is not reflected in the OSGi or Maven configurations. This means that it would only work with lfc, which is built using Gradle, not with Epoch or the LDS server (and thus VS Code).

For Maven there is this:

<dependency> <groupId>tools.aqua</groupId> <artifactId>z3-turnkey</artifactId> <version>4.8.16</version> </dependency>

I don't know how to fix the Eclipse configuration, to be honest. But we can't merge this until that is fixed because otherwise the project simply won't build in Eclipse.

Maybe @a-sr has any suggestions?

Added this to pom.xml, but Maven still doesn't work. I'm probably missing something obvious again...
But even if Maven works, there appears to be no way for this to work in Eclipse other than building Z3 from source and adding it to the build path. Everyone developing LF in Eclipse would have to do this to get a compiling code base. That doesn't sound great to me. Maybe publish a z3 lib OSGi bundle?

Alternatively, z3 could be included as a submodule. I expect this kind of problem to surface with other dependencies, too. And including a submodule for every library that isn't available as an OSGi bundle doesn't seem like a good solution either.

Yes, all non-plugin dependencies in Eclipse are tricky. If z3 is a compile-time dependency for Java, I guess there is no way around putting it in a plugin to make it work in Eclipse.
We also had this issue in Klighd with the Sprotty library that is only available on maven central. We created a repository to wrap it into a plugin (sprotty-mirror). The build automatically pulls the library, builds it into a plugin, and deploys it as an update site, such that we can use it in our Eclipse and Oomph setup as dependency. Maybe we need something similar for LF.
The official Eclipse Orbrit works with the same principle.

Regarding the dependency you added to the pom file, I do not know why this does not work or if that even will work. In the maven configuration, the option to consider pom dependencies in addition to the target platform is enables but I do not know how it works in detail. The current configuration has something to do with the workaround for Kotlin, but to be honest I am not sure how all these configurations work together.
Sorry.

lhstrh · 2022-05-25T00:48:12Z

org.lflang/src/org/lflang/generator/c/scheduling/uclid/SmtScheduleGenerator.java

+THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+***************/
+
+package org.lflang.generator.c;


Incorrect package declaration. That said, I'm not sure this is the right place to put this generator. It generates UCLID code, so I think it should be in a separate uclid package.

Thanks. Will put that in a separate uclid package.

lsk567 · 2022-06-01T00:35:27Z

@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 · 2022-06-01T04:19:59Z

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?

Soroosh129 reviewed May 23, 2022

View reviewed changes

lhstrh reviewed May 24, 2022

View reviewed changes

lhstrh reviewed May 25, 2022

View reviewed changes

lsk567 force-pushed the quasi-static-scheduler branch from f39097d to 407436c Compare June 14, 2022 05:58

lsk567 force-pushed the quasi-static-scheduler branch from 407436c to 81876ac Compare July 5, 2022 22:50

Implement a schedule generator for a QS scheduler.

f19ec04

lsk567 force-pushed the quasi-static-scheduler branch from 81876ac to f19ec04 Compare September 7, 2022 00:48

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Experimental] Quasi-static scheduler #1190

[Experimental] Quasi-static scheduler #1190

lsk567 commented May 23, 2022

Soroosh129 May 23, 2022

lsk567 May 24, 2022

Soroosh129 May 23, 2022

Soroosh129 May 23, 2022

lsk567 May 24, 2022 •

edited

Loading

Soroosh129 May 23, 2022

lsk567 May 24, 2022

lsk567 commented May 24, 2022

lhstrh May 24, 2022

lhstrh May 24, 2022

lhstrh May 24, 2022

lhstrh May 25, 2022 •

edited

Loading

lhstrh May 25, 2022

a-sr May 25, 2022

lhstrh May 25, 2022

lsk567 May 31, 2022

lsk567 commented Jun 1, 2022

lhstrh commented Jun 1, 2022

[Experimental] Quasi-static scheduler #1190

Are you sure you want to change the base?

[Experimental] Quasi-static scheduler #1190

Conversation

lsk567 commented May 23, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lsk567 May 24, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lsk567 commented May 24, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lhstrh May 25, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lsk567 commented Jun 1, 2022

lhstrh commented Jun 1, 2022

lsk567 May 24, 2022 •

edited

Loading

lhstrh May 25, 2022 •

edited

Loading