Improve --jobs UI

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

kani-driver/src/harness_runner.rs

@@ -103,30 +103,48 @@ 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}");
+            }
         }
     }
 
     fn should_print_output(&self) -> bool {
         !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);
         let prefix = path.parent().unwrap();
 
         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)
     }