Parallelized Verification

[emlaufer]

Hello again,

I was just wondering level of parallelism we should expect for each stage of the verification. For example, we are noticing that only one z3 instance is created, even though we would expect that parts of the verification could happen in parallel with different z3 instances. Thank you.

[vakaras]

Hello, the encoding is sequential and I doubt we will be able to parallelize this part until the compiler fully supports that. Regarding parallelization of verification: @fpoli I recall that there was a bug in the backend preventing us executing it in parallel, do you know whether that one is fixed? 2022-02-11, pn 00:23, Evan Laufer ***@***.***> rašė:

…

Hello again, I was just wondering level of parallelism we should expect for each stage of the verification. For example, we are noticing that only one z3 instance is created, even though we would expect that parts of the verification could happen in parallel with different z3 instances. Thank you. — Reply to this email directly, view it on GitHub <#857>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAASMU7R7LPZ6WEIMWW22JTU2RCGNANCNFSM5OCNHTSQ> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[fpoli]

Viper is not fully thread safe because of rare issues such as viperproject/silicon#578, but starting multiple prusti-server, each with its own JVM and Viper instance, would surely work. So, I see two options:

1. Make Prusti spread verification requests in a pool of prusti-server processes. For example, changing the PRUSTI_SERVER_ADDRESS configuration to a PRUSTI_SERVER_ADDRESSES that accepts a list of addresses. The client code to change is around the following lines.

   prusti-dev/prusti-viper/src/verifier.rs

   Lines 391 to 396 in 66c90d5

   	let client = PrustiClient::new(&server_address).unwrap_or_else(|error| {
   	panic!(
   	"Could not parse server address ({}) due to {:?}",
   	server_address, error
   	)
   	});

2. Ignore that Viper is not (yet) fully thread safe and add an experimental Prusti flag to run verifications in parallel. Then, fix Viper one data race at a time until it's effectively thread safe. Adding the experimental feature is quite easy on the Prusti side:
   • Make the server process multiple requests at the same time, replacing the basic_scheduler with a threaded_scheduler.

     prusti-dev/prusti-server/src/server.rs

     Lines 101 to 109 in 66c90d5

     	// Here we use a single thread because
     	// 1. Viper is not thread safe yet (Silicon issue #578), and
     	// 2. By default Silicon already uses as many cores as possible.
     	let mut runtime = Builder::new()
     	.basic_scheduler()
     	.thread_name("prusti-server")
     	.enable_all()
     	.build()
     	.expect("failed to construct Tokio runtime");

   • Replace the basic_scheduler with a threaded_scheduler on the client side too.

     prusti-dev/prusti-viper/src/verifier.rs

     Lines 397 to 405 in 66c90d5

     	// Here we construct a Tokio runtime to block until completion of the futures returned by
     	// `client.verify`. However, to report verification errors as early as possible,
     	// `verify_programs` should return an asynchronous stream of verification results.
     	let mut runtime = Builder::new()
     	.basic_scheduler()
     	.thread_name("prusti-viper")
     	.enable_all()
     	.build()
     	.expect("failed to construct Tokio runtime");

   • Parallelize this loop on the client side.

     prusti-dev/prusti-viper/src/verifier.rs

     Lines 424 to 427 in 66c90d5

     	verification_requests.map(|(program_name, request)| {
     	let result = process_verification_request(&viper_thread, request, &mut cache);
     	(program_name, result)
     	}).collect()

Option (1) is the most robust, but it has the disadvantage of starting multiple JVM instances and it wouldn't share the verification cache across prusti-server instances. I remember that other project started using Viper in concurrently, so we could join forces and go with option (2), fixing whatever doesn't work. The latter seems the best long-term solution to me.