Static Analysis of Memory Models for SMT Encodings (Video, OOPSLA2 2023)
Thomas Haas, René Maseli, Roland Meyer, and Hernán Ponce de León
(TU Braunschweig, Germany; TU Braunschweig, Germany; TU Braunschweig, Germany; Huawei, Germany)
Abstract: The goal of this work is to improve the efficiency of bounded model checkers that are modular in the memory model.
Our first contribution is a static analysis for the given memory model that is performed as a preprocessing step and helps us significantly reduce the encoding size.
Memory model make use of relations to judge whether an execution is consistent. The analysis computes bounds on these relations: which pairs of events may or must be related.
What is new is that the bounds are relativized to the execution of events.
This makes it possible to derive, for the first time, not only upper but also meaningful lower bounds.
Another important feature is that the analysis can import information about the verification instance from external sources to improve its precision.
Our second contribution are new optimizations for the SMT encoding.
Notably, the lower bounds allow us to simplify the encoding of acyclicity constraints.
We implemented our analysis and optimizations within a bounded model checker and evaluated it on challenging benchmarks.
The evaluation shows up-to 40% reduction in verification time (including the analysis) over previous encodings.
Our optimizations allow us to efficiently check safety, liveness, and data race freedom in Linux kernel code.
Article: https://doi.org/10.1145/3622855
Supplementary archive: https://doi.org/10.5281/zenodo.8313104 (Badges: Artifacts Available, Artifacts Evaluated — Functional)
ORCID: https://orcid.org/0000-0002-3176-8552, https://orcid.org/0000-0002-3608-2584, https://orcid.org/0000-0001-8495-671X, https://orcid.org/0000-0002-4225-8830
Video Tags: Abstract interpretation, weak memory models, bounded model checking, oopslab23main-p447-p, doi:10.1145/3622855, doi:10.5281/zenodo.8313104, orcid:0000-0002-3176-8552, orcid:0000-0002-3608-2584, orcid:0000-0001-8495-671X, orcid:0000-0002-4225-8830, Artifacts Available, Artifacts Evaluated — Functional
Presentation at the OOPSLA2 2023 conference, October 22–27, 2023, https://2023.splashcon.org/track/splash-2023-oopsla
Sponsored by ACM SIGPLAN,
Uh for the final Talk of the session uh Thomas hos is going to tell us about uh their work on static analysis of memory models for smt encodings yeah thank you for the introduction so my name is tomasas and this is Joint work with um my colleagues from T jik and Huawei
So um yeah let’s start with a typical verification approach say you’re given some program and you want to verify it against the specification and maybe you don’t even want to verify you just want to find Buck that’s good enough for now so you might employ a bounded model
Checking engine and the bounded model checking engine essentially takes the verification problem and translates it to a logical satisfiability problem and then uses some off the shelf um solving technique now if you usually a BMC engine is not just an encoder but it also uses something like a static
Analysis to either generate encoding in the first place or to generate more efficient encodings now if you want to argue about concurrent programs this problem gets a lot harder here because now we actually need to think about how threats communicate in concurrent programs and the answer to that is typically well
Over shared memory and now we get memory into the picture and memory needs what we call a memory model and now you want to take this memory model also as input to the uh verification task but now this opens up three questions first what are memory models
Second um how do we analyze these memory models and lastly well how do we encode them in this talk I’m going to uh answer the first two questions the third one is also a part of the paper but I don’t have time in this talk for this okay so
First of all what are concurrent program semantics now let’s look at this very uh simple program here it has two threads the left one and the right one and it works over shared memory the variables X and Y and somewhat atypical the semantics we associate to this program are actually
So-called execution graphs instead of what people usually do these inter leaving semantics so we look at graphs and these graphs have nodes which are called events essentially corresponding to the instructions of the program and then they have Rel that tell you how these events interact with each other such as how do they
Communicate for example we have the program order the black edges here which essentially just mimic the syntactic structure of the uh program so for example on the first graph you see um the right X1 is program ordered before the read to Y which is just the essentially the syntactic structure of
The program right then there’s a coherence order which I just explained on on an example here um you see the let’s take the first graph here um initially the memory value of x is set to zero and at some later point in time this value is overwritten and set to one
And this is what the coherence order essentially models the order in which the memory is overwritten each memory cell has its own coherence order that’s why X and Y here are independent and lastly there’s this read from order which just tells you where does the load take its value
From okay so it connects the load and the store now you might be wondering if you look at the first execution is this actually possible like can this happen you see both threats here read the value zero but if you then try to come up with an interleaving that leads to this value
Uh the the this outcome you will say this is not possible because one of the threats starts first and sets some m value to one then the other one cannot see this anymore right but then you can also say well well yes of course this outcome is surely possible because maybe
Your compiler reorders the code during compilation since it thinks these accesses are independent or the CPU does out of order execution and just executes the code in a different order now to model this we um used so-called memory models or the full name Memory consistency models and they simply answer the question
Given a program uh execution is it consistent with how the memory works with how the say the buffer structure of the memory works the and how the CPU reorders executions and so on and the idea is simply to look at the shape of these graphs and of these
Execution graphs and make a judgment based solely on the shape not on the data in the graphs and there exists a language to formulate these memory models called the cat language now we need to take a quick look at the cat language so the essential idea is to take these
Relations you already have these we call them base relations like the program order the read from and the coherence but they can be more and then simply Define new ones using relation algebra so you can Union them up you can intersect those relations whatsoever one problem is that you can
Also do introduce recursion so you can uh get nasty relations there and lastly you can formulate um constraints on these relations such as some relation has to be acyclic if this constraint is not satisfied then the execution is invalid with respect to the memory model it’s not consistent with a memory model
That’s the idea to look at an example here’s the sequential consistency model which amounts to the idea of inter leaving instructions and if we look at the execution graph there and then simply evaluate the relations we get to the following happens before relation graph you don’t need to follow why it
Looks like that but I mean it’s relation algebra Union just some unions and compositions right um then we can evaluate the a or the constraint the acyclicity constraint and it says well this cannot happen so this is invalid this execution is not allowed to happen
Okay but then if you look at more realis memory models that um incorporate say St buffering effects of actual Hardware then you will find out oh sorry there’s a little mistake on the slide I don’t know why um so the real some real models will say this is
Perfectly fine with how the memory Works due to store buffering effects you can get this strange outcome okay that’s the idea of the cat language now what we okay now you combine this um semantics with how the with a program and you simply cut off all the executions that do not um are
Inconsistent with respect to the memory model and this is how you get sort of the combined semantics of program plus memory model okay so now we want to do static analysis and we want want to do some very simple static analysis actually given the program and this cap model we
Simply want to find lower and upper bounds for all these relations over all possible executions so you can think of this as an interval abstraction but on the level of relations instead of like integers for example now here is a very simple example say we have this set of three execution
Graphs the um lower and upper bonds would look like this for example for the read from relation there’s not a single read from Edge that is common among all these graphs so the lower bound is empty the upper bound is simply four possible edges that you collect from all
These graphs together okay on the other hand for coherence and the program order you will see all these graphs match so you have an upper bound and lower bound are equal there’s no difference okay of course you can also do this um for these derived relations in the memory model so
You can also find lower and upper bonds for um the from read that happens before relation okay now this it looks very simple the this abstract main but there’s a little trick here because if we look at the lower bounds um we might ask the following question say we have this program here
Which has conditional execution which is typical in all programs right you have some conditional branching and look at the two following um execution graphs that are potentially um in that are in the semantics of the program you might say well the lower bound of the program order relation is the this AB
Edge because this is the one common among all the graphs right um but this notion is too strong because most code and programs is conditional so you will never really find too many edges that are really common among all program executions because they simply execute different uh
Code so what we did is we relativized this notion of lower bound to just say such an um Edge in the lower bound means this Edge is always there under the assumption that the um given that the events are executed in the first place so this is lower bound is sort of
Relational it’s it connects the edge variables or these edges to the execution of the events okay so this then also requires us to incorporate some control flow reasoning to um work over this domain now let’s look at abstract computation so we have our domain and now we want to compute things the idea
Is that the program um restricts the base relations because like a read um from X can only um read a value from a store to X but not from a store to Y so for example you can exploit alas information you can exploit alas information to um get information about
The the read from relation about the bounce on the re from relation and in general you can incorporate many program analysis to give some restriction on the base relations and then these restrictions is what we propagate upwards to the derived relations and interestingly the derived relations are then also constrained by
The memory model um constraints and this is something we can propagate downwards and this is what we did in our um work to give you an example there’s a very trivial program it’s not even concurrent so there’s no magic it’s arbitrary code um but it has these six events okay
If you unroll the loop three times um in the beginning the uper and lower bounds are trivial I’m not going to give you the full graph because I mean you don’t see much it’s the complete graph but then we take the program uh information is input and it
Tells us the following the program order is fixed so we have a lower bound that is precise because the syntax is fixed so the program order is fixed and but with respect to read from and coherence we don’t know much so these dashed edges are the upper bound
Okay everything can connected can be connected with everything else now we can derive uh propagate this information upwards and get the following happens before graph of possible happens before relationships now we can evaluate the acyclicity aim and that tells us none of these back edges are actually possible because they
Would contradict the lower bound we have for the forward edges so we get we would get a cycle so all of them are gone and now we can propagate this information also upwards again uh downwards sorry and remove all the backward edges in the original relations so there can
Not be any backward coherences or backward read from edges interesting L we can now evaluate the program again because the coherence order is actually a total order it has to um order the store somehow and we just excluded one possibility so the other one must be true it is now part of
Our lower bound and interestingly also the second read you have here because it has only one possible Target where it can read from this one has also to get be to get fixed so it’s it’s a lower bound as well and you can do this thing again um
Propagate up and and down and eventually you will have it completely fixed which is no surprise because this is a single threaded program fully deterministic so um there’s nothing open in the end everything is fixed in in concurrent programs it’s not so we get actual differences between the low and the upper
Bound okay once we have this information we want to exploit it but well for that check our paper but we use it to generate more efficient uh smt encodings so let’s come to the evaluation we’ve implemented the analysis in our bounded model Checker datan which uh takes these memory models
As an input in addition to the program and dato already has some static analysis because without any St static analysis the problem does not work at all like solving it is not going to work but this all static analysis was not founded on abstract interpretation so it
Was ad hoc um it had no lower bounds and that had not did not have the idea of propagating information top down just bottom up and it has uh two different solving strategies one which generates a full encoding and one which does uh generate an encoding iteratively in a lazy
Way now to give you a sort of the gist of the evaluation um we have evaluated this on verifying locks and lock free data structures under the arm and risk memory model as well as uh kernel code of of the Linux kernel memory model and if you
Look at the red boxes the top box is always the old Val the old result in of the verification time without our new analysis and the um lowest row is the the Improvement so for example for arm we could verify our test suit uh in 20 minutes instead of uh 30
Minutes and on the Linux kernel me in the Linux kernel we also got an hour faster and the eager encoding and even the lazy encoding scheme had some profits from this static analysis um okay to summarize we give a new abstract domain for relations it’s admittedly an easy domain but with a
Little twist on the lower bounds and we give an abstract interpretation based uh bir directional analysis analysis in the sense that it propagates information upwards and downwards and we show how to use it to improve the smt encodings thank you okay we have time for a couple of
Questions in terms of the evaluation can you go back a little bit um yeah sure quick question what are you verifying here where is the okay so yeah so uh we used c c implementation of locks and lock free data structures and we compil them down to arm and risk and for locks
We check if they if Mutual exclusion holds okay and for lock fre data structures we essentially check that multiple push and pop operations say do do not interfere so um if you have multiple threats that are pushing no note gets lost during the push everything comes to the uh and how how
Large is the code for for some how many line let’s say in lines of code it’s hard to say I mean q spin lock is from a Linux kernel so it has hundreds of lines of code um the other ones they’re quite small um but we used like four threads
And so we we scaled it in the terms of number of threads number of memory events that are happening so store and load operations it should be around between 100 and 200 load and store operations um yeah uh okay I I’ll I’ll ask a question I was trying to think about how you
Would handle loops and recursion because then you’re going to have a cycle just in the control flow so do you have to do your bounded unrolling and then do the abstract interpretation I mean sure so we do this after the unrolling since we do bounded model checking but otherwise
You would have to um say U maybe I can show on some um if you had such a graph you could start to merge nodes together so if you have a loop you just have one representative for all uh the the occurrences of this event so you compact it but then well
The bounce will be less accurate of course right but this should mean that you never have to do any widening or anything like that because you don’t have any cylic control flow no we always reduce it to some finite setting I would say and then so we don’t need to do this
Yeah any other questions Sor okay let’s thank the speaker again