Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Harness output individual files #3360

Merged
Merged
Changes from 1 commit
Commits
Show all changes
35 commits
Select commit Hold shift + click to select a range
2d1d29d
Starting changes for multi-thread attempt
Alexander-Aghili May 23, 2024
1387cb1
Buggy- revert
Alexander-Aghili May 23, 2024
81e6dfc
Threading implemented
Alexander-Aghili May 23, 2024
406a4ed
File output for each harness
Alexander-Aghili May 23, 2024
767b61b
Merge branch 'main' of github.com:model-checking/kani into main
Alexander-Aghili May 23, 2024
ba3090a
Update to add directory
Alexander-Aghili Jun 20, 2024
72522bc
Added individual output to files + args, still issues with directory …
Alexander-Aghili Jul 19, 2024
5b85c39
Harness refactor + directory fix
Alexander-Aghili Jul 19, 2024
0a40e1b
Quick format fix and refactor to fix the output correctness
Alexander-Aghili Jul 19, 2024
6a951b4
Refactor of harness runner update for Harness Output Individual Files
Jul 23, 2024
01bd260
Untested configuration options change (commit to get to server to test)
Alexander-Aghili Jul 31, 2024
2524fa1
Remove enable-unstable requirement
Alexander-Aghili Jul 31, 2024
1e125f4
Comments + formatting
Alexander-Aghili Aug 4, 2024
8b008c4
Merge branch 'main' into harness_output_individual_files
jaisnan Aug 5, 2024
38b6698
Merge branch 'main' into harness_output_individual_files
jaisnan Aug 12, 2024
cca9648
Update kani-driver/src/harness_runner.rs
celinval Aug 14, 2024
698d718
Merge branch 'main' into harness_output_individual_files
jaisnan Aug 14, 2024
56159a1
Merge branch 'main' into harness_output_individual_files
jaisnan Aug 20, 2024
1f0a0fd
merge
Alexander-Aghili Sep 18, 2024
78733a0
Merge branch 'main' into harness_output_individual_files
Alexander-Aghili Oct 7, 2024
c86ff09
Added test + fix small formatting with harness runner
Alexander-Aghili Oct 7, 2024
34f8c80
Remove target
Alexander-Aghili Oct 8, 2024
d35c664
Merge branch 'main' into harness_output_individual_files
jaisnan Oct 8, 2024
c3546c0
Fix clippy issues
Alexander-Aghili Oct 13, 2024
f9cddfa
Merge branch 'harness_output_individual_files' of github.com:Alexande…
Alexander-Aghili Oct 13, 2024
37ed122
Output directory name fix
Alexander-Aghili Oct 15, 2024
666a818
Remove old test unrelated to PR
Alexander-Aghili Oct 15, 2024
1593d23
Fix clippy issues (again)
Alexander-Aghili Oct 15, 2024
395ba91
Fixed test
Alexander-Aghili Oct 24, 2024
8dfde5d
Add mut back in builder creation
Alexander-Aghili Oct 24, 2024
f6b1527
Added comment, lets CI run
Alexander-Aghili Oct 24, 2024
fcadb6b
Merge branch 'main' into harness_output_individual_files
celinval Nov 4, 2024
b331bd6
Remove extra line
celinval Nov 4, 2024
016757d
Merge branch 'main' into harness_output_individual_files
celinval Nov 4, 2024
519d115
Merge branch 'main' into harness_output_individual_files
celinval Nov 5, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Threading implemented
Alexander-Aghili committed May 23, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
commit 81e6dfc30da800beeeca928b92ee4c68815fb4a1
15 changes: 11 additions & 4 deletions kani-driver/src/harness_runner.rs
Original file line number Diff line number Diff line change
@@ -8,6 +8,7 @@ use std::path::Path;
use std::thread;
use std::sync::mpsc;
use std::sync::Arc;
use std::time::Instant;

use crate::args::OutputFormat;
use crate::call_cbmc::{VerificationResult, VerificationStatus};
@@ -44,14 +45,18 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> {
self.check_stubbing(harnesses)?;

let sorted_harnesses = crate::metadata::sort_harnesses_by_loc(harnesses);

let max_threads = 8;
let pool = {
let mut builder = rayon::ThreadPoolBuilder::new();
if let Some(x) = self.sess.args.jobs() {
builder = builder.num_threads(x);
let mut threads = sorted_harnesses.len();
if threads > max_threads {
threads = max_threads;
}
builder = builder.num_threads(threads);
builder.build()?
};

let before = Instant::now();

let results = pool.install(|| -> Result<Vec<HarnessResult<'pr>>> {
sorted_harnesses
@@ -74,7 +79,9 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> {
.collect::<Result<Vec<_>>>()
})?;

Ok(results)
println!("Elapsed Time: {:.2?}\n", before.elapsed());

Ok(results)
}

/// Return an error if the user is trying to verify a harness with stubs without enabling the