Finish initial draft of the Alloy article.

This commit is contained in:
Danila Fedorin 2023-05-14 21:13:23 -07:00
parent 384f5de765
commit 23cf7c9e8b
5 changed files with 170 additions and 75 deletions

View File

@ -124,7 +124,7 @@ pred possibleState[filterState: FilterState] {
// If it's a method receiver, add method or field restriction // If it's a method receiver, add method or field restriction
addBitfieldFlag[bitfieldMiddle, filterState.curFilter, MethodOrField] or addBitfieldFlag[bitfieldMiddle, filterState.curFilter, MethodOrField] or
// if it's not a receiver, filter to non-methods (could be overridden) // 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. // Maybe methods are not being curFilterd but it's not a receiver, so no change.
bitfieldEqual[bitfieldMiddle, filterState.curFilter] bitfieldEqual[bitfieldMiddle, filterState.curFilter]
} }
@ -174,26 +174,29 @@ fact step {
} }
} }
example: run { counterexampleNotFound: run {
all searchState: SearchState { all searchState: SearchState {
// a way that subsequent results of searching it will miss things. // a way that subsequent results of searching will miss things.
eventually some symbol: Symbol, fs: FilterState, fsBroken: FilterState, exclude: Bitfield { eventually some symbol: Symbol,
fs: FilterState, fsBroken: FilterState,
exclude1: Bitfield, exclude2: Bitfield {
// Some search (fs) will cause a transition / modification of the search state... // Some search (fs) will cause a transition / modification of the search state...
possibleState[fs] possibleState[fs]
updateOrSet[searchState.found, fs] updateOrSet[searchState.found, fs]
excludeBitfield[searchState.found, exclude1]
// Such that a later, valid search... (fsBroken) // Such that a later, valid search... (fsBroken)
possibleState[fsBroken] possibleState[fsBroken]
excludeBitfield[searchState.found', exclude] excludeBitfield[searchState.found', exclude2]
// Will allow for a symbol ... // Will allow for a symbol ...
// ... that are left out of the original search... // ... that are left out of the original search...
not bitfieldMatchesProperties[searchState.found, symbol] not bitfieldMatchesProperties[searchState.found, symbol]
// ... and out of the current search // ... 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... // But would be matched by the broken search...
bitfieldMatchesProperties[fsBroken.curFilter, symbol] bitfieldMatchesProperties[fsBroken.curFilter, symbol]
// ... to not be matched by a search with the new state: // ... 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])
} }
} }
} }

Binary file not shown.

After

Width:  |  Height:  |  Size: 134 KiB

Binary file not shown.

After

Width:  |  Height:  |  Size: 158 KiB

Binary file not shown.

After

Width:  |  Height:  |  Size: 154 KiB

View File

@ -2,15 +2,18 @@
title: "Proving My Compiler Code Incorrect With Alloy" title: "Proving My Compiler Code Incorrect With Alloy"
date: 2023-05-02T22:48:52-07:00 date: 2023-05-02T22:48:52-07:00
tags: ["Compilers", "Alloy"] tags: ["Compilers", "Alloy"]
expirydate: 2022-04-22T12:19:22-07:00
draft: true draft: true
--- ---
{{< todo >}}
Intro section and disclaimer
{{< /todo >}}
I work as a compiler developer on the [Chapel](https://chapel-lang.org) team. 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 ### The Problem at Hand
One of the things that a language like Chapel has to do is called _resolution_, 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 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 possible cases, I realized that it would be much nicer to describe this
mathematically, and have a model checker generate outlandish scenarios for mathematically, and have a model checker generate outlandish scenarios for
me. Having at some point seen [Hillel Wayne's me.
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.
### Modeling Flags and Bitsets in Alloy ### Modeling Flags and Bitsets in Alloy
Flags are represented on the C++ side as an `enum` (with custom indexing so 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 `initialState`, the model of our C++ code can end up with its particular
set of flags in the `curFilter` bitfield. set of flags in the `curFilter` bitfield.
### Modeling Search State
Next, I needed to model the behavior the I described earlier: searching for 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. when running subsequent searches.
Dyno implemented this roughly as follows: 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 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 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 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: behavior in Alloy:
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 147 150 >}} {{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 147 150 >}}
The first line of the predicate represents the second item from the list If you look closely, this predicate uses a feature of Alloy we haven't
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
really seen: its ability to reason about time by dipping into _temporal logic_. 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 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 `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 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 the _next moment in time_.
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`.
{{< todo >}} The first line of the predicate represents the second item from the list
The rest of the article above: if a scope hasn't been searched before (represented by the _present_
{{< /todo >}} 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 {{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 138 140 >}}
{{< todo >}}
This section is temporary
{{< /todo >}}
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, With the `updateOrSet` predicate in hand, we can actually specify how our
{{< sidenote "right" "notation-note" "we could denote the claim" >}} model will evolve. To do so, we first need to specify the initial
This is in no way standard notation; I'm making it up as I go along. conditions. In particular, our scope will start out not having been
{{< /sidenote >}} searched; its flags will be `NotSet`.
that some state \\(A\\) is changed to state \\(B\\) by a statement \\(s\\)
as follows:
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 ```Chapel
module M { module TopLevel {
module XContainerUser {
} public use TopLevel.XContainer; // Will search for public, to no avail.
``` }
module XContainer {
private var x: int;
```Chapel {linenos=true} record R {} // R is in the same scope as x so it won't set public
module M1 { module MethodHaver {
public use super.M2; use TopLevel.XContainerUser;
} use TopLevel.XContainer;
module M2 { proc R.foo() {
private var x = 1; var y = x;
}
module M3 {
public use super;
} }
}
} }
use M1;
use M2.M3;
writeln(x)
``` ```
Alas, the two-bitfield system is not just an approximation, it malfunctions
Moreover, a `public use` makes these definitions part in practice. I submitted a PR to fix the issue.
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