diff --git a/alloy/alloy-blog.png b/alloy/alloy-blog.png
new file mode 100644
index 0000000..8fc64f7
Binary files /dev/null and b/alloy/alloy-blog.png differ
diff --git a/alloy/slides.md b/alloy/slides.md
index 5a7ce64..b54da45 100644
--- a/alloy/slides.md
+++ b/alloy/slides.md
@@ -29,25 +29,15 @@ Daniel Fedorin, HPE
---
-# Terms
-
-* What are **formal methods**?
- * Techniques rooted in computer science and mathematics to specify and verify systems
-* What part of the **Chapel compiler**?
- * The 'Dyno' compiler front-end, particularly its use/import resolution phase.
- * This piece is used by the production Chapel compiler.
-
----
-
# The Story
I have a story in three parts.
1. I found it very hard to think through a section of compiler code.
- - Specifically, code that performed lookups in `use`s/`import`s
+ - Specifically, code that performed scope lookups for variables
2. I used the [Alloy Analyzer](https://alloytools.org/) to model the assumptions and behavior of the code.
- - I had little background in Alloy, but some background in (formal) logic
+ - I had little background in Alloy, but some background in formal logic
3. This led me to discover a bug in the compiler that I then fixed.
- Re-creating the bug required some gymnastics that were unlikely to occur in practice.
@@ -66,11 +56,388 @@ Imagine you see the following snippet of Chapel code:
foo();
```
-Where do you look for `foo`? The answer is quite complicated, and depends
-strongly on the context of the call.
+Where do you look for `foo`? The answer is quite complicated, and depends strongly on the context of the call.
+
+Moreover, the order of where to look matters: method calls are preferred over global functions, "nearer" functions are preferred over "farther" ones.
+
+---
+
+# The Humble `foo` (example 1)
+
+```chapel
+module M1 {
+ record R {}
+
+ proc R.foo() { writeln("R.foo"); }
+ proc foo() { writeln("M1.foo"); }
+
+ proc R.someMethod() {
+ foo(); // which 'foo'?
+ }
+}
+```
+
+* Both `R.foo` and `M1.foo` would be valid candidates.
+* We give priority to methods over global functions. So, the compiler would:
+ * Search `R` and its scope (`M1`) for methods named `foo`.
+ * If that fails, search `M1` for any symbols `foo`.
+* We've had to look at `M1` twice! (once for methods, once for non-methods)
+
+---
+
+# The Humble `foo` (example 2)
+
+```chapel
+module M1 {
+ record R {}
+
+ proc foo() { writeln("R.foo"); }
+}
+module M2 {
+ use M1;
+
+ proc R.someMethod() {
+ foo(); // which 'foo'?
+ }
+}
+```
+
+Here, we search the scope of `R` and `M1`, but **only for public symbols**.
+
+---
+
+
+# How Chapel's Compiler Handles This
+
+We want to:
+- Respect the priority order
+ - Including preferring methods over non-methods
+ - As a result, we search the scopes multiple times
+- Avoid any extra work
+ - This includes redundant re-searches
+ - Example redundant search: looked up "all symbols", then later "all public symbols"
+
+---
+
+# Encoding Search Configuration
+
+```C++
+enum { PUBLIC = 1, NOT_PUBLIC = 2, METHOD_FIELD = 4, NOT_METHOD_FIELD = 8, /* ... */ };
+```
+
+1. For each scope, save the flags we've already searched with
+2. When searching a scope again, exclude the flags we've already searched with
+
+This was handled by two bitfields: `filter` and `excludeFilter`.
+
+---
+
+# Populating `filter` and `excludeFilter`
+
+```C++
+if (skipPrivateVisibilities) { // depends on context of 'foo()'
+ filter |= IdAndFlags::PUBLIC;
+}
+
+else if (!includeMethods && receiverScopes.empty()) {
+ filter |= IdAndFlags::NOT_METHOD;
+}
+```
+
+```C++
+excludeFilter = previousFilter;
+```
+
+```C++
+// scary!
+previousFilter = filter & previousFilter;
+```
+
+Code notes `previousFilter` is an approximation.
+
+---
+# Possible Problems
+
+* `previousFilter` is an approximation.
+* However, no case we knew of hit this combination of searches, or any like it.
+ * All of our language tests passed.
+ * Code seemed to work.
+* If only there was a way I could get a computer to check whether such a combination
+ could occur...
+
+---
+
+
+# Formal Methods
+
+---
+
+# Model Checking
+
+Model checking involves formally describing the behavior of a system, then having a solver check whether other desired properties hold.
+ - Alloy is an example of a model checker.
+ - TLA is another famous example.
+
+---
+
+# A Primer on Logic (example)
+
+Model checkers like Alloy are rooted in temporal logic, which builds on first-order logic.
+
+Example statement: "Bob has a son who likes all compilers".
+
+$$
+\exists x. (\text{Son}(x, \text{Bob}) \land \forall y. (\text{Compiler}(y) \Rightarrow \text{Likes}(x, y)))
+$$
+
+In Alloy:
+
+```alloy
+some x { Son[x, Bob] and all y { Compiler[y] implies Likes[x, y] } }
+```
+
+---
+
+# A Primer on Temporal Logic
+
+Temporal logic provides additional operators to reason about how properties change over time.
+
+- $\Box p$ (in Alloy: `always p`): A statement that is always true.
+ - Example: $\Box(\text{like charges repel})$
+- $\Diamond p$ (in Alloy: `eventually p`) : A statement that will be true at some point in the future.
+ - Example: $\Diamond(\text{the sun is in the sky})$
+
+In Alloy specifically, we can mention the next state of a variable using `'`.
+
+```alloy
+// pseudocode:
+// the next future value of previousFilter will be the intersection of filter
+// and the current value
+previousFilter' = filter & previousFilter;
+```
+
+---
+
+# Modeling Possible Searches
+
+Alloy isn't an imperative language. We can't mutate variables like we do in C++. Instead, we model how each statement changes the state, by relating the "current" state to the "next" state.
+
+
+
+
+```C++
+ filter |= IdAndFlags::PUBLIC;
+```
+
+
+
+
+```alloy
+ addBitfieldFlag[filterNow, filterNext, Public]
+```
+
+
+
+
+
+```C++
+ curFilter |= IdAndFlags::PUBLIC;
+ curFilter |= IdAndFlags::METHOD_FIELD;
+```
+
+
+
+
+```alloy
+ addBitfieldFlag[filterNow, filterNext1, Public]
+ addBitfieldFlag[filterNext1, filterNext2, Method]
+```
+
+
+
+
+
+```C++
+ if (skipPrivateVisibilities) {
+ curFilter |= IdAndFlags::PUBLIC;
+ }
+
+ if (!includeMethods && receiverScopes.empty()) {
+ curFilter |= IdAndFlags::NOT_METHOD;
+ }
+```
+
+
+
+```alloy
+ addBitfieldFlag[initialState.curFilter, bitfieldMiddle, Public] or
+ bitfieldEqual[initialState.curFilter, bitfieldMiddle]
+
+
+ // if it's not a receiver, filter to non-methods (could be overridden)
+ addBitfieldFlagNeg[bitfieldMiddle, filterState.curFilter, Method] or
+ bitfieldEqual[bitfieldMiddle, filterState.curFilter]
+```
+
+
+
+
+```chapel
+module TopLevel {
+ module XContainerUser {
+ public use TopLevel.XContainer;
+ }
+ module XContainer {
+ private var x: int;
+ record R {}
+ module MethodHaver {
+ use TopLevel.XContainerUser;
+ use TopLevel.XContainer;
+ proc R.foo() {
+ var y = x;
+ }
+ }
+ }
+}
+```
+
+
+
+* the scope of `R` is searched with for methods
+* The scope of `R`’s parent (`XContainer`) is searched for methods
+* The scope of `XContainerUser` is searched for public symbols (via the `use`)
+* The scope of `XContainer` is searched with public symbols (via the `public use`)
+* The scope of `XContainer` searched for with no filters via the second use; but the stored filter is bad, so the lookup returns early, not finding `x`.
+
+
+
-
-
-```C++
- filter |= IdAndFlags::PUBLIC;
-```
-
-
-
-
-```alloy
- addBitfieldFlag[filterNow, filterNext, Public]
-```
-
-
-
-
-
-```C++
- curFilter |= IdAndFlags::PUBLIC;
- curFilter |= IdAndFlags::METHOD_FIELD;
-```
-
-
-
-
-```alloy
- addBitfieldFlag[filterNow, filterNext1, Public]
- addBitfieldFlag[filterNext1, filterNext2, Method]
-```
-
-
-
-
-
-```C++
- if (skipPrivateVisibilities) {
- curFilter |= IdAndFlags::PUBLIC;
- }
-
-
-
-
-
-
- if (onlyMethodsFields) {
- curFilter |= IdAndFlags::METHOD_FIELD;
- } else if (!includeMethods && receiverScopes.empty()) {
- curFilter |= IdAndFlags::NOT_METHOD;
- }
-
-
-
-```
-
-
-
-```alloy
- addBitfieldFlag[initialState.curFilter, bitfieldMiddle, Public] or
- bitfieldEqual[initialState.curFilter, bitfieldMiddle]
-
-
-
-
-
-
-
- // 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
-
- // Maybe methods are not being curFilterd but it's not a receiver, so no change.
- bitfieldEqual[bitfieldMiddle, filterState.curFilter]
-```
-
-
-
-
-```chapel
-module TopLevel {
- module XContainerUser {
- public use TopLevel.XContainer;
- }
- module XContainer {
- private var x: int;
- record R {}
- module MethodHaver {
- use TopLevel.XContainerUser;
- use TopLevel.XContainer;
- proc R.foo() {
- var y = x;
- }
- }
- }
-}
-```
-
-
-
-* the scope of `R` is searched with for methods
-* The scope of `R`’s parent (`XContainer`) is searched for methods
-* The scope of `XContainerUser` is searched for public symbols (via the `use`)
-* The scope of `XContainer` is searched with public symbols (via the `public use`)
-* The scope of `XContainer` searched for with no filters via the second use; but the stored filter is bad, so the lookup returns early, not finding `x`.
-
-
-
+
+
+ ```Chapel
+ record C1 { type arg1; /* ... */ type argi; }
+ // ...
+ record Cn { type arg1; /* ... */ type argj; }
+ ```
+
+
+
+ ```Haskell
+ data T = C1 arg1 ... argi
+ | ...
+ | Cn arg1 ... argj
+ ```
+
+
+
+
+```Chapel
+
+proc insert(type t: Empty, param x: int) type do return Node(x, Empty, Empty);
+proc insert(type t: Node(?v, ?left, ?right), param x: int) type do
+ select true {
+ when x < v do return Node(v, insert(left, x), right);
+ otherwise do return Node(v, left, insert(right, x));
+ }
+
+type test = insert(insert(insert(Empty, 2), 1), 3);
+
+
+
+proc lookup(type t: Empty, param x: int) param do return false;
+proc lookup(type t: Node(?v, ?left, ?right), param x: int) param do
+ select true {
+ when x == v do return true;
+ when x < v do return lookup(left, x);
+ otherwise do return lookup(right, x);
+ }
+```
+
+
+
+```Haskell
+insert :: Int -> BSTree -> BSTree
+insert x Empty = Node x Empty Empty
+insert x (Node v left right)
+
+ | x < v = Node v (insert x left) right
+ | otherwise = Node v left (insert x right)
+
+
+test = insert 3 (insert 1 (insert 2 Empty))
+
+
+lookup :: Int -> BSTree -> Bool
+lookup x Empty = False
+lookup x (Node v left right)
+
+ | x == v = True
+ | x < v = lookup x left
+ | otherwise = lookup x right
+
+```
+
+
-
-
- ```Chapel
- record C1 { type arg1; /* ... */ type argi; }
- // ...
- record Cn { type arg1; /* ... */ type argj; }
- ```
-
-
-
- ```Haskell
- data T = C1 arg1 ... argi
- | ...
- | Cn arg1 ... argj
- ```
-
-
-
-
-```Chapel
-
-proc insert(type t: Empty, param x: int) type do return Node(x, Empty, Empty);
-proc insert(type t: Node(?v, ?left, ?right), param x: int) type do
- select true {
- when x < v do return Node(v, insert(left, x), right);
- otherwise do return Node(v, left, insert(right, x));
- }
-
-type test = insert(insert(insert(Empty, 2), 1), 3);
-
-
-
-proc lookup(type t: Empty, param x: int) param do return false;
-proc lookup(type t: Node(?v, ?left, ?right), param x: int) param do
- select true {
- when x == v do return true;
- when x < v do return lookup(left, x);
- otherwise do return lookup(right, x);
- }
-```
-
-
-
-```Haskell
-insert :: Int -> BSTree -> BSTree
-insert x Empty = Node x Empty Empty
-insert x (Node v left right)
-
- | x < v = Node v (insert x left) right
- | otherwise = Node v left (insert x right)
-
-
-test = insert 3 (insert 1 (insert 2 Empty))
-
-
-lookup :: Int -> BSTree -> Bool
-lookup x Empty = False
-lookup x (Node v left right)
-
- | x == v = True
- | x < v = lookup x left
- | otherwise = lookup x right
-
-```
-
-