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 https://github.com/viperproject/prusti-dev/issues/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 https://github.com/viperproject/silicon/issues/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. https://github.com/viperproject/prusti-dev/blob/66c90d5dae9040eb68b2f0d2689faa480b10e8d6/prusti-viper/src/verifier.rs#L391-L396
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. https://github.com/viperproject/prusti-dev/blob/66c90d5dae9040eb68b2f0d2689faa480b10e8d6/prusti-server/src/server.rs#L101-L109
   • [ ] Replace the basic_scheduler with a threaded_scheduler on the client side too. https://github.com/viperproject/prusti-dev/blob/66c90d5dae9040eb68b2f0d2689faa480b10e8d6/prusti-viper/src/verifier.rs#L397-L405
   • [ ] Parallelize this loop on the client side. https://github.com/viperproject/prusti-dev/blob/66c90d5dae9040eb68b2f0d2689faa480b10e8d6/prusti-viper/src/verifier.rs#L424-L427

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.