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,29 +174,26 @@ fact step {
     }
 }
 
-counterexampleNotFound: run {
+example: run {
     all searchState: SearchState {
-        // a way that subsequent results of searching will miss things.
-        eventually some symbol: Symbol,
-                        fs: FilterState, fsBroken: FilterState,
-                        exclude1: Bitfield, exclude2: Bitfield {
+        // a way that subsequent results of searching it will miss things.
+        eventually some symbol: Symbol, fs: FilterState, fsBroken: FilterState, exclude: 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', exclude2]
+            excludeBitfield[searchState.found', exclude]
 
             // 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[exclude1, symbol])
+            not (bitfieldMatchesProperties[fs.curFilter, symbol] and not bitfieldMatchesProperties[searchState.found, 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[exclude2, symbol])
+            not (bitfieldMatchesProperties[fsBroken.curFilter, symbol] and not bitfieldMatchesProperties[exclude, symbol])
         }
     }
 }

content/blog/dyno_alloy/index.md

@@ -2,25 +2,15 @@
 title: "Proving My Compiler Code Incorrect With Alloy"
 date: 2023-05-02T22:48:52-07:00
 tags: ["Compilers", "Alloy"]
-description: "In this post, I apply Alloy to a piece of code in the Chapel compiler to find a bug."
+expirydate: 2022-04-22T12:19:22-07:00
 draft: true
 ---
 
-__Disclaimer:__ though "my compiler code" makes for a fun title, I do not
-claim exclusive credit for any of the C++ code in the Chapel compiler that
-I mention in this post. The code is "mine" in the sense that I was
-debugging changes I was making, and perhaps also in the sense that I was
-working with it.
+{{< 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_,
@@ -212,7 +202,11 @@ 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.
+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.
 
 ### Modeling Flags and Bitsets in Alloy
 Flags are represented on the C++ side as an `enum` (with custom indexing so
@@ -590,10 +584,8 @@ 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 past searches
+\\(A \\land \\lnot B\\), and taking the intersection of two past searches
 when running subsequent searches.
 
 Dyno implemented this roughly as follows:
@@ -624,170 +616,79 @@ 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
-simple predicate that implemented the "store if not set, intersect if set"
+similar predicate that implemented the "store if not set, intersect if set"
 behavior in Alloy:
 
 {{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 147 150 >}}
 
-If you look closely, this predicate uses a feature of Alloy we haven't
+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
 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_.
+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 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:
+{{< todo >}}
+The rest of the article
+{{< /todo >}}
 
-{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 138 140 >}}
+### Scratch Work
+{{< 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`.
 
-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`.
+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: 
 
-{{< 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.
+a small-ish program to illustrate what I mean.
 
 ```Chapel
-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;
-      }
-    }
-  }
+module M {
+    
 }
 ```
 
-Alas, the two-bitfield system is not just an approximation, it malfunctions
-in practice. I submitted a PR to fix the issue.
+
+```Chapel {linenos=true}
+module M1 {
+    public use super.M2;
+}
+module M2 {
+    private var x = 1;
+
+    module M3 {
+        public use super;
+    }
+}
+
+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