diff --git a/code/dyno-alloy/DynoAlloy.als b/code/dyno-alloy/DynoAlloy.als index 4b3c5c4..c984169 100644 --- a/code/dyno-alloy/DynoAlloy.als +++ b/code/dyno-alloy/DynoAlloy.als @@ -124,7 +124,7 @@ pred possibleState[filterState: FilterState] { // If it's a method receiver, add method or field restriction addBitfieldFlag[bitfieldMiddle, filterState.curFilter, MethodOrField] or // if it's not a receiver, filter to non-methods (could be overridden) - addBitfieldFlagNeg[bitfieldMiddle, filterState.curFilter, Method] or + // addBitfieldFlagNeg[bitfieldMiddle, filterState.curFilter, Method] or // Maybe methods are not being curFilterd but it's not a receiver, so no change. bitfieldEqual[bitfieldMiddle, filterState.curFilter] } @@ -174,26 +174,29 @@ fact step { } } -example: run { +counterexampleNotFound: run { all searchState: SearchState { - // a way that subsequent results of searching it will miss things. - eventually some symbol: Symbol, fs: FilterState, fsBroken: FilterState, exclude: Bitfield { + // a way that subsequent results of searching will miss things. + eventually some symbol: Symbol, + fs: FilterState, fsBroken: FilterState, + exclude1: Bitfield, exclude2: Bitfield { // Some search (fs) will cause a transition / modification of the search state... possibleState[fs] updateOrSet[searchState.found, fs] + excludeBitfield[searchState.found, exclude1] // Such that a later, valid search... (fsBroken) possibleState[fsBroken] - excludeBitfield[searchState.found', exclude] + excludeBitfield[searchState.found', exclude2] // Will allow for a symbol ... // ... that are left out of the original search... not bitfieldMatchesProperties[searchState.found, symbol] // ... and out of the current search - not (bitfieldMatchesProperties[fs.curFilter, symbol] and not bitfieldMatchesProperties[searchState.found, symbol]) + not (bitfieldMatchesProperties[fs.curFilter, symbol] and not bitfieldMatchesProperties[exclude1, symbol]) // But would be matched by the broken search... bitfieldMatchesProperties[fsBroken.curFilter, symbol] // ... to not be matched by a search with the new state: - not (bitfieldMatchesProperties[fsBroken.curFilter, symbol] and not bitfieldMatchesProperties[exclude, symbol]) + not (bitfieldMatchesProperties[fsBroken.curFilter, symbol] and not bitfieldMatchesProperties[exclude2, symbol]) } } } diff --git a/content/blog/dyno_alloy/bug.png b/content/blog/dyno_alloy/bug.png new file mode 100644 index 0000000..193c3da Binary files /dev/null and b/content/blog/dyno_alloy/bug.png differ diff --git a/content/blog/dyno_alloy/bug_2.png b/content/blog/dyno_alloy/bug_2.png new file mode 100644 index 0000000..af1dd25 Binary files /dev/null and b/content/blog/dyno_alloy/bug_2.png differ diff --git a/content/blog/dyno_alloy/bug_3.png b/content/blog/dyno_alloy/bug_3.png new file mode 100644 index 0000000..3d70f37 Binary files /dev/null and b/content/blog/dyno_alloy/bug_3.png differ diff --git a/content/blog/dyno_alloy/index.md b/content/blog/dyno_alloy/index.md index a89d688..04e0f46 100644 --- a/content/blog/dyno_alloy/index.md +++ b/content/blog/dyno_alloy/index.md @@ -2,15 +2,18 @@ title: "Proving My Compiler Code Incorrect With Alloy" date: 2023-05-02T22:48:52-07:00 tags: ["Compilers", "Alloy"] -expirydate: 2022-04-22T12:19:22-07:00 draft: true --- -{{< todo >}} -Intro section and disclaimer -{{< /todo >}} - I work as a compiler developer on the [Chapel](https://chapel-lang.org) team. +Recently, while thinking through a change to some code, I caught myself +making wishes: "if only I could have a computer check this property for +me". Having at some point seen [Hillel Wayne's post](https://www.hillelwayne.com/post/alloy6/) +about the release of [Alloy 6](https://alloytools.org/), I thought I'd give it +a go. In this post, I describe my experience applying Alloy to a real part of +the Chapel compiler. I'd never touched Alloy before this, so be warned: this +is what I came up with on my own attempt, and I may well be doing something +fairly silly by the standards of "real" Alloy users. ### The Problem at Hand One of the things that a language like Chapel has to do is called _resolution_, @@ -202,11 +205,7 @@ That is, until I decided that it was time to add another possible flag to the bitfield. At that point, sitting and trying to reason about the possible cases, I realized that it would be much nicer to describe this mathematically, and have a model checker generate outlandish scenarios for -me. Having at some point seen [Hillel Wayne's -post](https://www.hillelwayne.com/post/alloy6/) about the release of -[Alloy 6](https://alloytools.org/), I thought I'd give it a go. I'd never -touched Alloy before this, so be warned: this is what I came up with on my -own attempt. +me. ### Modeling Flags and Bitsets in Alloy Flags are represented on the C++ side as an `enum` (with custom indexing so @@ -584,8 +583,10 @@ There's not much more to the predicate. It says, in English, that a state `initialState`, the model of our C++ code can end up with its particular set of flags in the `curFilter` bitfield. +### Modeling Search State + Next, I needed to model the behavior the I described earlier: searching for -\\(A \\land \\lnot B\\), and taking the intersection of two past searches +\\(A \\land \\lnot B\\), and taking the intersection of past searches when running subsequent searches. Dyno implemented this roughly as follows: @@ -616,79 +617,170 @@ Both of these signatures use a new keyword, `one`. This keyword means that there's only a single instance of both `NotSet` and `SearchState` in our model. This is in contrast to a signature like `Bitfield,` which allows multiple bitfields to exist at the same time. I ended up with a pretty -similar predicate that implemented the "store if not set, intersect if set" +simple predicate that implemented the "store if not set, intersect if set" behavior in Alloy: {{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 147 150 >}} -The first line of the predicate represents the second item from the list -above: if a scope hasn't been searched before, the new value is just the -current filter / bitfield. The second line handles the third item: -updating a previously-set filter based on new flags. I defined an -additional predicate to help with this: - -{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 138 140 >}} - -At first, this predicate doesn't seem like much. However, if you look -closely, this single-line predicate uses a feature of Alloy we haven't +If you look closely, this predicate uses a feature of Alloy we haven't really seen: its ability to reason about time by dipping into _temporal logic_. Notice that the predicate is written not just in terms of `toSet`, but also `toSet'`. The tick (which I personally read as "prime") indicates that what we're talking about is not the _current_ value of `toSet`, but its value at -the _next moment in time_. What this predicate says, then, is that _at the next -moment_, the value of `toSet` will be equal to its present value, -intersected with `curFilter`. I also had to specify that `toSet'`, the -future value of `toSet`, will still be a Bitfield after the step, and would -not revert to a `NotSet`. +the _next moment in time_. -{{< todo >}} -The rest of the article -{{< /todo >}} +The first line of the predicate represents the second item from the list +above: if a scope hasn't been searched before (represented by the _present_ +value of `toSet` being `NotSet`) the future value (represented by `toSet'`) +is just the current filter / bitfield. The second line handles the third item +from the list, updating a previously-set filter based on new flags. I defined +an additional predicate to help with this: -### Scratch Work -{{< todo >}} -This section is temporary -{{< /todo >}} +{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 138 140 >}} +What this predicate says is that _at the next moment_, the value of `toSet` +will be equal to its present value intersected with `curFilter`. I also had +to specify that the future value of `toSet`, will still be a +`Bitfield` after the step, and would not revert to a `NotSet`. -More abstractly, -{{< sidenote "right" "notation-note" "we could denote the claim" >}} -This is in no way standard notation; I'm making it up as I go along. -{{< /sidenote >}} -that some state \\(A\\) is changed to state \\(B\\) by a statement \\(s\\) -as follows: +With the `updateOrSet` predicate in hand, we can actually specify how our +model will evolve. To do so, we first need to specify the initial +conditions. In particular, our scope will start out not having been +searched; its flags will be `NotSet`. -a small-ish program to illustrate what I mean. +{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 138 140 >}} + +Next, we must specify that our `SearchState` changes in a very particular +way: each step, the code invokes a search, and the state is modified to +record that the search occurred. Each search is described via `curFilter` +in a `filterState`. We want to ensure that `curFilter` is a reasonable +filter (that is, it's a combination of flags that can actually arise in the +C++ program). To ensure this, we can use the `possibleState` predicate from +earlier. From there, the `updateOrSet` predicate can be used to specify +that this step's `curFilter` is saved, either as-is (if no searches +occurred previously) or as an intersection (if this is not the first +search). The whole fact corresponding to this is below: + +{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 161 175 >}} + +### Asking for Counterexamples + +As we've already seen, Alloy works by finding examples: combinations of +various variables that match our requirements. It won't be sufficient to +ask Alloy for an example of our code doing what we expect: if the code +malfunctions nine times out of ten, Alloy will still find us the one case +in which it works. It won't tell us much. + +Instead, we have to ask it to find a _counterexample_: a case which does +_not_ work. If Alloy succeeds in finding such an example, the code we're +modeling has a bug. Of course, to make all this work, you need to know what +to ask. There's no way to tell Alloy, "find me a bug" -- we need to be more +specific. I had to focus on bugs I was most worried about. + +If the stored combination of flags (in `found`) evolves into a bad +configuration, things can go wrong in two ways. The first is that we will +somehow exclude symbols from the lookup that shouldn't have been excluded. +In other words, can past searches break future searches? + +I came up with the following Alloy (counter)example to model this +situation. It's a little bit long; there are comments there to explain what +it does, and I'll go through below. + +{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 177 202 >}} + +This example asks that at some point in time, things "go wrong". In +particular, will there by a symbol (`symbol`) that hasn't been found yet, +such that a search for a particular filter (`fs`) will break the system, +making a subsequent search `fsBroken` not find `symbol` even though it +should have? + +The `possibleState`, `updateOrSet`, and `excludeBitfield` +lines encode the fact that a search occurred for `fs`. This must be a valid +search, and the search state must be modified appropriately. Furthermore, +at the time this search takes place, to make the \\(\\lnot B\\) portion of +the algorithm work, the bitfield `exclude1` will be set based on the +previous search state. + +The next two lines, `possibleState` and `excludeBitfield`, set the stage for +the broken search: `fsBroken` is a another valid search, and at the time it +happens, the bitfield `exclude2` is set based on previous search state. +Since `fsBroken` occurs after `fs`, its "previous search state" is actually +the state _after_ `fs`, so we use `found'` instead of `found`. + +Finally, the subsequent four lines of code describe the issue: the symbol +in question has not been found before `fs`, and nor will it be found by +`fs`. That means thus far, it hasn't been reported to the user. +Therefore, if the symbol matches `fsBroken`, it ought to be reported: we haven't +seen it yet, and here we're being asked for something matching the symbol's +description! However, as per the last line of code, searching for +`fsBroken` together with the appropriate set of exclude flags, we still +don't find `symbol`. That's a problem! + +Unfortunately, Alloy finds a model that satisfies this constraint. There +are a lot of moving parts, so the output is a bit difficult to read. I did +my best to clean it up by turning off some arrows. Our system is spanning +multiple "moments" in time, so a single picture won't describe the bug +entirely. Here's the diagram Alloy outputs for the first state: + +{{< figure src="bug.png" caption="Figure representing the initial state according to Alloy" class="fullwide" >}} + +We can get a lot out of this figure. First, the symbol-to-be-lost is a +private method (it doesn't have the `PPublic` property, and it does have +the `PMethod` property). Also, Alloy immediately gives away what `fs` and +`fsBroken` will be: eventually, when the user searches for all +_non-methods_ (`negativeFlags: Method` are the giveaway there), their +subsequent search for _anything_ will fail to come up with our private +method, even though it should. To gather more details about this broken +case, we can look at the state that follows the initial one. + +{{< figure src="bug_2.png" caption="Figure representing the second state according to Alloy" class="fullwide" >}} + +The main difference is that `found` has changed from `NotSet` (because no +searches occurred) to `FilterState1`. This indicates that the first search +was for all `Public` symbols (which our method is not). There is only one +more state after this: + +{{< figure src="bug_3.png" caption="Figure representing the final state according to Alloy" class="fullwide" >}} + +In the above diagram, `found` has changed once again, this time to an empty +bitfield. This is a valid behavior for our system. Recall that `fs` was a +search for non-methods, and that the intersection of `NOT_METHOD` and `PUBLIC` +is empty. Thus, `found` will be set to the empty `bitfield`, which +(incorrectly) indicates that all symbols have been searched for! After +this, any search would fail: `fsBroken` doesn't have any flags set, and +still, nothing is reported. + +Now, this doesn't definitively prove the compiler is broken: it's possible +that there isn't a situation in which three searches like this (`PUBLIC`, +then `NOT_METHOD`, then anything) will occur in practice. However, this +gave the "motif" for reproducing the bug. All I had to do was find a +real-life case that matched the counterexample. + +It was a little easier to find a reproducer for a similar counterexample, +actually. By inspection, I noticed that the same bug would occur if the +second search was for `METHOD_OR_FIELD`, and not for `NOT_METHOD`. I was +able to come up with a (fairly convoluted) example of Chapel code that +triggered the issue. I include it here as a curiosity; there's no need to +understand how exactly it works. ```Chapel -module M { - -} -``` - - -```Chapel {linenos=true} -module M1 { - public use super.M2; -} -module M2 { - private var x = 1; - - module M3 { - public use super; +module TopLevel { + module XContainerUser { + public use TopLevel.XContainer; // Will search for public, to no avail. + } + module XContainer { + private var x: int; + record R {} // R is in the same scope as x so it won't set public + module MethodHaver { + use TopLevel.XContainerUser; + use TopLevel.XContainer; + proc R.foo() { + var y = x; + } } + } } - -use M1; -use M2.M3; -writeln(x) ``` - - Moreover, a `public use` makes these definitions part -of the module that does the `use` -- that is, `M1` would now contain the -definitions from `M2`. However, since `M1` is not defined inside of `M2`, it -isn't able to access its private variables (like `x` on line 5), so this -particular use statement leaves `M1` just containing (a reference to) `M3`. - -The `public use` on line +Alas, the two-bitfield system is not just an approximation, it malfunctions +in practice. I submitted a PR to fix the issue.