Automated Verification of Parallel Nested DFS
This is a modal window.
The media could not be loaded, either because the server or network failed or because the format is not supported.
Formal Metadata
| Title |
| |
| Title of Series | ||
| Number of Parts | 22 | |
| Author | ||
| Contributors | ||
| License | CC Attribution 3.0 Germany: You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor. | |
| Identifiers | 10.5446/55012 (DOI) | |
| Publisher | ||
| Release Date | ||
| Language |
Content Metadata
| Subject Area | ||
| Genre | ||
| Abstract |
| |
| Keywords |
00:00
Model checkingMathematical modelMathematical modelKolmogorov complexityAlgorithmParameter (computer programming)Proof theoryFormal verificationConnectivity (graph theory)Parallel portAlgorithmMereologySemiconductor memoryFunctional (mathematics)Codierung <Programmierung>Overhead (computing)Connectivity (graph theory)Latent heatCategory of beingParameter (computer programming)Mathematical optimizationBounded variationModel checkingAdditionProof theoryExtension (kinesiology)Mathematical modelSeries (mathematics)Formal verificationPresentation of a groupComplex (psychology)Mechanism designLoop (music)ExistenceCodeBitGraph (mathematics)Revision controlContext awarenessPhysical systemGraph (mathematics)State of matterSpacetimeComputer animation
02:45
Parallel portAutomatonModel checkingSequenceCodeInterior (topology)Complete metric spaceStrategy gameParallel computingClefDepth-first searchState of matterDepth-first searchMathematical modelLinearizationSet (mathematics)Thread (computing)Cycle (graph theory)Revision controlMultiplication signAlgorithmGraph (mathematics)Basis <Mathematik>outputState of matterGraph coloringArithmetic meanAutomatonCentralizer and normalizerSequenceData structureMereologyDifferent (Kate Ryan album)Finite setComplete metric spaceCategory of beingInterior (topology)TheoryInstance (computer science)Constructor (object-oriented programming)Model checkingCASE <Informatik>Parameter (computer programming)BacktrackingGraph (mathematics)Standard deviationParallel portArrow of timeArithmetic progressionCartesian coordinate systemPhysical systemComputer animation
08:30
Parameter (computer programming)Invariant (mathematics)Parallel portFormal verificationConcurrency (computer science)Computer programSequenceRead-only memoryFunctional (mathematics)Parameter (computer programming)Formal verificationCodeGraph coloringInvariant (mathematics)Multiplication signPattern languageCycle (graph theory)SynchronizationFreewareLine (geometry)Thread (computing)Proof theorySemiconductor memoryConfiguration spaceMathematical optimizationAlgorithmParallel portConnectivity (graph theory)SequenceComputer programmingModal logicRevision controlAutomationNumberState of matterGraph (mathematics)Concurrency (computer science)Set (mathematics)Computer animation
11:47
State of matterThread (computing)OvalRootRaster graphicsContext awarenessLocal ringFlagBoolean algebraFrequencyPredicate (grammar)Nachlauf <Strömungsmechanik>Fluid staticsOperations researchDepth-first searchParallel portInvariant (mathematics)CodeParalleler AlgorithmusTraverse (surveying)Random numberMechatronicsFormal verificationType theoryRadical (chemistry)EmailVertex (graph theory)IntelRevision controlMatrix (mathematics)Reading (process)PermianFlow separationPredicate (grammar)1 (number)Computer programmingCycle (graph theory)Category of beingComplete metric spaceParallel portLemma (mathematics)Position operatorThread (computing)Operator (mathematics)Local ringAlgorithmGraph coloringState of matterInterior (topology)Codierung <Programmierung>MereologyInvariant (mathematics)Design by contractConcurrency (computer science)Multiplication signLoop (music)Semiconductor memoryInformationFunctional (mathematics)Computer animation
13:31
Formal verificationTotal S.A.Graph (mathematics)Zoom lensLemma (mathematics)Function (mathematics)Proof theoryCodeOverhead (computing)Latent heatInteractive televisionCodierung <Programmierung>Identical particlesTheoremDifferent (Kate Ryan album)Combinational logicFunctional (mathematics)MereologyLemma (mathematics)Category of being1 (number)Formal verificationLine (geometry)CodeConcurrency (computer science)Direction (geometry)Graph (mathematics)Computer fileBitComputer programmingMeta elementSlide ruleTotal S.A.Flow separationSemiconductor memoryComputer animationXML
15:17
Formal verificationGraph (mathematics)Parallel portAlgorithmDepth-first searchFunctional (mathematics)Computer fileFormal verificationAlgorithmComputer animation
Transcript: English(auto-generated)
00:01
Hello everyone, my name is Wietse Ortwijn, and I'm going to talk about the work we did on the automated verification of the Parallel Nesta-Deadfast Search Graph Algorithm. This is joint work with Madika Heusmann, Sebastian Jooster and Jakob van der Poel. As the name suggests, Parallel Nesta-DFS is a parallelized version of Nesta-DFS, which in turn is a model checking algorithm.
00:25
So the context of this work is a model checking. Model checkers are used to verify properties of reactive systems. In order to do that reliably, it is crucial that model checking algorithms are themselves correct. However, correctness of such algorithms is highly non-trivial, as model checking algorithms are
00:44
often paralyzed and heavily optimized to be able to go quickly through large state spaces. But this comes at a price. As the complexity of model checkers increases, so does the difficulty in achieving that correctness. Proving the correctness of model checking algorithms is a big challenge.
01:01
As far as we are aware, no mechanical verifications of parallel model checking algorithms exist. To the best of our knowledge, this work contributes the first mechanical verification of a parallel model checking algorithm, Parallel N-DFS. The verification is carried out in the automated code verifier FairCore.
01:22
We encoded Parallel N-DFS in FairCore's verification language, and specified all correctness properties as pre- and post-condition annotations, loop invariants, etc. FairCore then automatically proves correctness of the algorithm. Mechanizing the correctness argument of Parallel N-DFS was highly non-trivial.
01:41
We had to rephrase the original handwritten proof quite a bit to make it suitable for proof mechanization. Ultimately, we verified memory safety, race freedom, and full functional correctness of Parallel N-DFS. Our FairCore formalization consists of reusable components that can be used to verify variations of the algorithm.
02:01
We demonstrate this by also verifying two optimizations of Parallel N-DFS with little additional effort. In particular, we propose a fix to one of these extensions by adding a check that was missing in the original paper. The remainder of this presentation consists of three parts.
02:22
First, I will give some background on Parallel N-DFS. I will illustrate how the algorithm works and why its correctness is so difficult to establish. In part 2, I will go into our approach for mechanically verifying Parallel N-DFS with FairCore. I will also show the actual FairCore encoding and highlight some interesting parts.
02:40
After that, in part 3, I will briefly discuss specification overhead. The N-DFS algorithm operates an automata, which are the central data structure in this talk. An automaton is a directed graph consisting of a finite set of nodes that are connected via edges. Exactly one of the nodes is marked as initial, in this case as 1, which is indicated by the flying incoming arrow.
03:06
Nodes can also be marked as accepting, which is indicated by a double border. Here S1 and S3 are accepting. Automata have many important applications. One of them is LTL model checking, checking whether some system model M satisfies an LTL property phi.
03:24
It has been shown that, under certain assumptions, the LTL model checking problem can be reduced to the following. Automata theoretic problem, no reachable accepting cycles exist in a particular automata construction that involves both M and phi. An accepting cycle is a cycle that includes an accepting state, like for example the one shown here.
03:45
And then the accepting cycle is said to be reachable if it can be reached from the initial state, like so. Nested depth-first search is a linear time algorithm for finding reachable accepting cycles. This algorithm forms the basis of the spin model checker.
04:03
And the FS-first does an outer depth-first search that searches for accepting states. And every time it encounters an accepting state while backtracking, an inner depth-first search is started from that state to search for any cycles. Let me show an example run, starting from S1. NDFS uses colors to indicate the status of exploration, where light blue means partially explored by the outer search.
04:28
From S1, the outer search may go down and explore S4 and S5. It cannot explore further now, so S5 will be marked dark blue, which means fully explored by the outer search. S4 will be marked as well, after which exploration continues to S2, S3 and S6.
04:47
S6 is now fully explored, and so the outer search will backtrack to S3. But since S3 is accepting, an inner search is started before backtracking further, to search for cycles. Now S3 has two colors, one for the outer search and one for the inner search.
05:04
This nested search uses pink to indicate partial exploration, and red to indicate full exploration. The inner search may fully explore all blue nodes, like so, before it finds S2, and thereby an accepting cycle.
05:23
Here you see sequential NDFS in pseudocode. Both the outer and inner searches are just standard instances of DFS, and indeed maintain their progress with color sets. We are interested in proving the correctness of paralyzed versions of NDFS, where correct means sound and complete.
05:41
The property of soundness is that if NDFS reports a cycle, then it must be an accepting one. And completeness means that if there exists an accepting cycle, then NDFS will report it. One naive way to paralyze NDFS is by a technique called swarming.
06:01
The idea of swarming is simple. You spawn N-parallel instances of NDFS, each working on a private set of colors. Different threads might then choose to explore different parts of the input graph in a hope to find accepting cycles faster. However, threads don't cooperate, as they now each have their own color set. So if the input graph, for example, doesn't have any accepting cycles,
06:24
then this swarmed version might actually be slower than the sequential version. Larman et al., among others, found a way to make threads cooperate, and thereby improve on his swarming approach. They proposed a parallel NDFS algorithm, which is the algorithm that is central in our work, and also used in the LTSMin model checker.
06:46
The key idea is to make the red colorings shared, and to skip red states during both the outer and inner search. By doing so, threads avoid exploring parts of the graph that have already been explored by others, and this leads to speed up.
07:02
However, sharing the red colorings also significantly complicates the correctness argument. Not only do threads now cooperate, they can actually now hinder each other. By coloring a state red, a thread may actually block the detection of accepting cycles. Let me show an example of this.
07:21
Suppose that we execute parallel NDFS on this automata with two threads, T1 and T2. Suppose that T1 gets scheduled first, and starts exploring left. So it sees as 1, S4, S5, S6, backtracks, then starts an inner search as it
07:40
backtracks on an accepting state, which will explore S4, S5, S6, and finally colors S6 red. Now suppose that thread 2 gets scheduled. So we switch to the colorings that thread 2 can see, which is only red since red states are shared now. Thread 2 could explore right, in which case it sees S2, S3, and that's it since S6 will now be skipped.
08:07
And since thread 2 backtracks on an accepting state, it will start an inner search. And this inner search will immediately complete since red states are skipped. So as a result, S3 will become red, which means that this accepting cycle, S2, S3, S6, S5, will never be found.
08:25
We say that this cycle is thus obstructed. Let us now go into the argument of why parallel NDFS is correct, and our approach to mechanize this argument in the faircore code verifier.
08:43
The original paper of Larman et al. contains a hand-written, complicated correctness argument stating that not all accepting cycles can be missed in such a way. However, this argument is not an inductive one, and therefore not directly suitable for mechanization. So we first had to rephrase the correctness argument to make it inductive.
09:03
I will not explain this new correctness argument in detail, but let me try to give an outline. We started by identifying a number of invariants on our color configurations. To give an example, we've already seen that any inner search can only explore states that are already blue or cyan.
09:21
Most of the coloring variants have been taken from the original paper of Larman, but we also needed an extra one to be able to close our new proof. We showed that our coloring variants halt by proving that every line of the algorithm preserves them. From these coloring variants, we can prove that, under certain conditions, there must exist paths in the graph that have certain coloring patterns.
09:44
We call these paths special paths, and they are an important ingredient for mechanically proving completeness. In particular, these special paths allow proving that every time an accepting cycle is obstructed, there must exist another accepting cycle that is not yet obstructed.
10:03
This implies that not all accepting cycles can be missed, which is used to prove completeness. If we go back to our earlier situation, we can indeed see that there is another accepting cycle, namely this one. This accepting cycle cannot be obstructed and will eventually be detected if the algorithm would continue to execute.
10:27
After writing our new pen and paper proof, we continued by mechanizing it using Faircore. Faircore is an automated code verifier that is specialized in reasoning about concurrent programs. For the verification, we took an incremental approach.
10:42
We started by porting an already existing Daphne verification of sequential NDFS to Faircore as a stepping stone to further verification. We then adopted this sequential version to perform swarmed NDFS to get some initial parallelization. This verification of swarmed NDFS was straightforward after having verified the
11:02
sequential version, as every thread works on their own disjoint color set. We continued by sharing the red colorings and adding the necessary thread synchronization to get to parallel NDFS. As expected, this step drastically complicated the verification. First, we proved that parallel NDFS is memory safe and free of data races.
11:24
Then we encoded the coloring invariants and proved that every line of the algorithm preserves them. After that, we encoded all arguments and proofs around a special path and used these to close the correctness proof. Finally, we verified two optimizations of parallel NDFS with very little additional effort.
11:44
We thereby demonstrated our verification components are reusable. Let me show you the actual Faircore encoding of parallel NDFS. I'll not manage to go through everything of course, but I'll highlight some interesting parts. Here you first see several thread local fields, followed by several operations for updating node colorings.
12:09
Going down a bit, you'll find the inner search procedure, together with its contract and loop invariants. In a contract, you'll find the color invariants, for example that nodes cannot be pink and red at the same time.
12:26
Going down further, you'll also find the outer search. Here you see the lock invariant, which protects the ownership to all shared information.
12:43
These perm predicates that you see here are predicates of concurrent separation logic, and are used to establish memory safety and data race freedom. All properties about special paths are encoded as so-called lemma functions, like the ones shown here. Lemma functions are side-effect-free programs to which the lemma property is encoded as a contract.
13:06
There are quite many of them. And finally, here you see the main function, together with the soundness and completeness properties. If the algorithm returns positively, then there exists a node that is accepting, and is on an accepting cycle.
13:23
Completeness states deconference. If there exists a node that is accepting, and is on an accepting cycle, then the algorithm will return positively. Let us now very briefly discuss the amount of specification overhead. In order to do that, let me zoom out a bit.
13:42
Here you see the faircore verification file I just showed you, but now zoomed out enough to make it fit on one slide. This file is about 1270 lines of code, after removing several comments and empty lines and such, to make it fit better. Of these lines, roughly 240 encoding of the actual algorithm, so about 16% of the total.
14:07
This means that the rest of the file, about 84%, is specification, which is rather a lot. We can actually distinguish different kinds of specification.
14:20
Of the part highlighted now, about 460 lines are for encoding the properties of interest, so the ones for proving memory safety and full functional correctness. And all other lines of specification are for the encoding of the lemma functions and other properties that don't directly have to do with code execution. Like, for example, the properties related to special paths and for proving completeness.
14:45
We found that an automated code verifier really helped us in our verification. As code verifiers do a lot of work for you, you don't need to reason yourself about what happens after every execution step the program might take. However, I think that all the auxiliary lemmas and meta properties, the part that is highlighted now,
15:04
might be done more conveniently in an interactive theorem prover, like Isabelle or Coq. Therefore, I think that a combination of concurrent code verification and interactive theorem proving could be a very interesting direction of future research. To conclude, we present the first automated verification of a parallel graph algorithm, parallel nested that first search.
15:27
We hope that you now have an idea of what the algorithm does, why its correctness is so difficult to establish, and how we managed to mechanize the correctness proof. Thanks a lot for watching, and I'd be happy to answer any questions.