Add initial support for Litani build and dashboard. #389

bdalrhm · 2021-08-05T13:50:00Z

Description of changes:

This PR adds initial support for Litani build. We use Litani to run RMC on the examples and generate an HTML dashboard with the results.

Resolved issues:

Resolves #384 & #392

Call-outs:

src/tools/dashboard/src/util.rs contains a lot of duplicated code from compiletest. Consider reconciling with compiletest or porting all of our test suites to Litani.
We run the examples in the reference twice to generate the terminal dashboard and Litani's dashboard. Consider using run.json to generate the terminal dashboard.
The default names stages Litani uses (build, test, and report) does not match with our stages (check, codegen, verification). Switch to custom stage names when Litani adds support for that.

Testing:

How is this change tested?
- The generated HTML dashboard closely matches the terminal version.
Is this a refactor change?
- No.

Checklist

Each commit message has a non-empty body, explaining why the change was made
Methods or procedures are documented
Regression or unit tests are included, or existing tests cover the modified code
My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

adpaco-aws · 2021-08-05T14:35:30Z

src/tools/dashboard/src/litani.rs

+        for command in self.spawned_commands.iter_mut() {
+            command.wait().unwrap();
+        }


What if they do not terminate? Are we using timeouts when invoking litani?

We're not running the tests here. We're only adding them as jobs for Litani to run later. This command takes less around 0.1 second. However, the run-build command after this may not terminate, but that's a good hint that we're missing a --unwind argument somewhere.

Can we add a timeout to run-build then? Litani should have that feature.

Can do. Currently, individual jobs can take a --timeout flag which is often more useful, but added an issue for this.

adpaco-aws · 2021-08-05T14:38:38Z

src/tools/dashboard/src/litani.rs

+        command.get_envs().filter(|(k, _)| !job_envs.contains_key(k)).fold(
+            &mut new_envs,
+            |fmt, (k, v)| {
+                fmt.write_fmt(format_args!(
+                    "{}=\"{}\" ",
+                    k.to_str().unwrap(),
+                    v.unwrap().to_str().unwrap()
+                ))
+                .unwrap();
+                fmt
+            },
+        );


Is this block of code just pretty-printing a HashMap struct? There must be a more idiomatic way of doing that.

hmm... I haven't found anything online. I could use flat_map instead of fold if you prefer that.

adpaco-aws · 2021-08-05T14:45:14Z

src/tools/dashboard/src/util.rs

+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! The types and procedures in this modules are similar to the ones in
+//! `compiletest`. Consider using `Litani` to run the test suites.
+


We should import these types and procedures instead. Or add them here and import in compiletest.

Opened an issue for this.

adpaco-aws · 2021-08-05T14:48:31Z

src/tools/dashboard/src/litani.rs

+    /// A buffer of the `spawn`ed Litani jobs so far. `Litani` takes some time
+    /// to execute each `add-job` command and executing thousands of them
+    /// sequentially takes a considerable amount of time. To speed up the
+    /// execution of those commands, we spawn those commands sequentially (as
+    /// normal). However, instead of `wait`ing for each process to terminate,
+    /// we add its handle to a buffer of the `spawn`ed processes and continue
+    /// with our program. Once we are done adding jobs, we wait for all of them
+    /// to terminate before we run the `run-build` command.


We can just say that we spawn all litani asynchronously and wait for them to terminate.

.gitmodules

karkhaz · 2021-08-05T14:23:50Z

src/tools/dashboard/src/litani.rs

+    /// we add its handle to a buffer of the `spawn`ed processes and continue
+    /// with our program. Once we are done adding jobs, we wait for all of them
+    /// to terminate before we run the `run-build` command.
+    spawned_commands: Vec<Child>,


It's actually safe to run multiple litani add-job in parallel. Have you considered doing something like that? If there's a way in rust to launch some kind of thread pool, you could have a bunch of worker threads that all call litani add-job concurrently. We do this in other projects, but using python.

No need to do this for this PR, it could be something we do later.

That's what spawned_commands is for 🙂. We spawn the litani add-job processes sequentially. But the processes themselves run concurrently. I experimented with spawning those processes concurrently, but did not see any performance improvements as it takes much longer to execute and terminate litani add-job processes concurrently than it takes spawn them and parse all tests sequentially (it's Rust after all 😉).

karkhaz · 2021-08-05T20:08:25Z

src/tools/dashboard/src/litani.rs

+        for command in self.spawned_commands.iter_mut() {
+            command.wait().unwrap();
+        }


Can do. Currently, individual jobs can take a --timeout flag which is often more useful, but added an issue for this.

src/tools/dashboard/src/litani.rs

karkhaz · 2021-08-05T20:12:24Z

src/tools/dashboard/src/litani.rs

+            fmt
+        });
+        job.args([
+            "add-job",


If you're using inputs and outputs as I suggest below, I suggest also passing in --phony-outputs; this is available in the develop branch of Litani, we'll release it probably next week

That's SO COOOL!!!

src/tools/dashboard/src/util.rs

adpaco-aws

I think it is better to insert links instead of referencing issue numbers. This way developers can just click on them.

src/tools/dashboard/src/util.rs

adpaco-aws · 2021-08-06T16:44:57Z

src/tools/dashboard/src/litani.rs

+            "--ok-returns",
+            &exit_status.to_string(),
+            "--timeout",
+            "10",


We should avoid hard-coding here by making timeout a parameter of add_job.

Done! Changed the timeout value for check and codegen steps to 1 sec.

src/tools/dashboard/src/util.rs

* Add initial support for Litani build and dashboard. * Add panic message and issue numbers. * Add a timeout for Litani jobs. * Add depencies between jobs. * Add links to issues. Co-authored-by: Adrian Palacios <[email protected]>

bdalrhm added the Area: testing label Aug 5, 2021

bdalrhm self-assigned this Aug 5, 2021

bdalrhm requested review from adpaco-aws and karkhaz August 5, 2021 13:50

adpaco-aws suggested changes Aug 5, 2021

View reviewed changes

karkhaz reviewed Aug 5, 2021

View reviewed changes

bdalrhm linked an issue Aug 6, 2021 that may be closed by this pull request

Add dependencies between jobs in a test pipeline. #392

Closed

bdalrhm requested review from adpaco-aws and karkhaz August 6, 2021 15:58

adpaco-aws suggested changes Aug 6, 2021

View reviewed changes

bdalrhm added 5 commits August 6, 2021 18:57

Add initial support for Litani build and dashboard.

3f9fba8

Add panic message and issue numbers.

74e9aef

Add a timeout for Litani jobs.

70d2d27

Add depencies between jobs.

21fa35d

Add links to issues.

96107dc

bdalrhm force-pushed the litani branch from 9e8aacc to 96107dc Compare August 6, 2021 18:57

bdalrhm changed the base branch from main-154-2021-08-02 to main-154-2021-08-06 August 6, 2021 18:58

bdalrhm requested a review from adpaco-aws August 6, 2021 18:58

adpaco-aws approved these changes Aug 9, 2021

View reviewed changes

Merge branch 'main-154-2021-08-06' into litani

73e6042

bdalrhm merged commit 3d4a86e into model-checking:main-154-2021-08-06 Aug 9, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add initial support for Litani build and dashboard. #389

Add initial support for Litani build and dashboard. #389

bdalrhm commented Aug 5, 2021 •

edited

Loading

adpaco-aws Aug 5, 2021

bdalrhm Aug 5, 2021

adpaco-aws Aug 5, 2021 •

edited

Loading

karkhaz Aug 5, 2021

adpaco-aws Aug 5, 2021

bdalrhm Aug 5, 2021 •

edited

Loading

adpaco-aws Aug 5, 2021

bdalrhm Aug 5, 2021

adpaco-aws Aug 5, 2021

karkhaz Aug 5, 2021

bdalrhm Aug 6, 2021

karkhaz Aug 5, 2021

karkhaz Aug 5, 2021

bdalrhm Aug 6, 2021

adpaco-aws left a comment

adpaco-aws Aug 6, 2021

bdalrhm Aug 6, 2021

Add initial support for Litani build and dashboard. #389

Add initial support for Litani build and dashboard. #389

Conversation

bdalrhm commented Aug 5, 2021 • edited Loading

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

Choose a reason for hiding this comment

Choose a reason for hiding this comment

adpaco-aws Aug 5, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bdalrhm Aug 5, 2021 • 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

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

adpaco-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bdalrhm commented Aug 5, 2021 •

edited

Loading

adpaco-aws Aug 5, 2021 •

edited

Loading

bdalrhm Aug 5, 2021 •

edited

Loading