From 09f125fbd0d7202e8be93cb680cd2f8905772716 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Wed, 18 Dec 2024 15:57:07 -0500
Subject: [PATCH 1/3] improve --jobs docs & unhide it

---
 kani-driver/src/args/mod.rs | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
index 66ff247ddc82..9b2408d484e2 100644
--- a/kani-driver/src/args/mod.rs
+++ b/kani-driver/src/args/mod.rs
@@ -257,8 +257,11 @@ pub struct VerificationArgs {
     // consumes everything
     pub cbmc_args: Vec<OsString>,
 
-    /// Number of parallel jobs, defaults to 1
-    #[arg(short, long, hide = true, requires("enable_unstable"))]
+    /// Number of threads to spawn to verify harnesses in parallel.
+    /// Omit the flag entirely to run sequentially (i.e. one thread).
+    /// Pass -j to run with the thread pool's default number of threads.
+    /// Pass -j <N> to specify N threads.
+    #[arg(short, long, hide_short_help = true, requires("enable_unstable"))]
     pub jobs: Option<Option<usize>>,
 
     /// Enable extra pointer checks such as invalid pointers in relation operations and pointer

From 3ce002a380764ef38e8b58468dc270d7626dca1e Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Wed, 18 Dec 2024 15:57:23 -0500
Subject: [PATCH 2/3] print thread number if there's parallelization

---
 kani-driver/src/harness_runner.rs | 37 +++++++++++++++++++++++++------
 1 file changed, 30 insertions(+), 7 deletions(-)

diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
index ee14992cba78..2994ffcb0386 100644
--- a/kani-driver/src/harness_runner.rs
+++ b/kani-driver/src/harness_runner.rs
@@ -103,14 +103,23 @@ impl<'pr> HarnessRunner<'_, 'pr> {
 }
 
 impl KaniSession {
-    fn process_output(&self, result: &VerificationResult, harness: &HarnessMetadata) {
+    fn process_output(
+        &self,
+        result: &VerificationResult,
+        harness: &HarnessMetadata,
+        thread_index: usize,
+    ) {
         if self.should_print_output() {
             if self.args.output_into_files {
-                self.write_output_to_file(result, harness);
+                self.write_output_to_file(result, harness, thread_index);
             }
 
             let output = result.render(&self.args.output_format, harness.attributes.should_panic);
-            println!("{}", output);
+            if rayon::current_num_threads() > 1 {
+                println!("Thread {thread_index}: {}", output);
+            } else {
+                println!("{}", output);
+            }
         }
     }
 
@@ -118,7 +127,12 @@ impl KaniSession {
         !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old
     }
 
-    fn write_output_to_file(&self, result: &VerificationResult, harness: &HarnessMetadata) {
+    fn write_output_to_file(
+        &self,
+        result: &VerificationResult,
+        harness: &HarnessMetadata,
+        thread_index: usize,
+    ) {
         let target_dir = self.result_output_dir().unwrap();
         let file_name = target_dir.join(harness.pretty_name.clone());
         let path = Path::new(&file_name);
@@ -126,7 +140,11 @@ impl KaniSession {
 
         std::fs::create_dir_all(prefix).unwrap();
         let mut file = File::create(&file_name).unwrap();
-        let file_output = result.render(&OutputFormat::Regular, harness.attributes.should_panic);
+        let mut file_output =
+            result.render(&OutputFormat::Regular, harness.attributes.should_panic);
+        if rayon::current_num_threads() > 1 {
+            file_output = format!("Thread {thread_index}:\n{file_output}");
+        }
 
         if let Err(e) = writeln!(file, "{}", file_output) {
             eprintln!(
@@ -148,13 +166,18 @@ impl KaniSession {
         binary: &Path,
         harness: &HarnessMetadata,
     ) -> Result<VerificationResult> {
+        let thread_index = rayon::current_thread_index().unwrap_or_default();
         if !self.args.common_args.quiet {
-            println!("Checking harness {}...", harness.pretty_name);
+            if rayon::current_num_threads() > 1 {
+                println!("Thread {thread_index}: Checking harness {}...", harness.pretty_name);
+            } else {
+                println!("Checking harness {}...", harness.pretty_name);
+            }
         }
 
         let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?;
 
-        self.process_output(&result, harness);
+        self.process_output(&result, harness, thread_index);
         self.gen_and_add_concrete_playback(harness, &mut result)?;
         Ok(result)
     }

From 80442fc3167a8a57fe0f936efa735c8cec5bca08 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Wed, 18 Dec 2024 17:25:57 -0500
Subject: [PATCH 3/3] Apply suggestions from code review

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
---
 kani-driver/src/harness_runner.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
index 2994ffcb0386..b78e1dc9d80b 100644
--- a/kani-driver/src/harness_runner.rs
+++ b/kani-driver/src/harness_runner.rs
@@ -116,9 +116,9 @@ impl KaniSession {
 
             let output = result.render(&self.args.output_format, harness.attributes.should_panic);
             if rayon::current_num_threads() > 1 {
-                println!("Thread {thread_index}: {}", output);
+                println!("Thread {thread_index}: {output}");
             } else {
-                println!("{}", output);
+                println!("{output}");
             }
         }
     }