Finalize slides given timing constraints
Signed-off-by: Danila Fedorin <daniel.fedorin@hpe.com>
This commit is contained in:
Danila Fedorin
BIN
alloy/alloy-blog.png
Normal file
BIN
alloy/alloy-blog.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 1.9 KiB |
814
alloy/slides.md
814
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...
|
||||
|
||||
---
|
||||
|
||||
<!-- _class: lead -->
|
||||
# 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.
|
||||
|
||||
<div class="side-by-side">
|
||||
<div>
|
||||
|
||||
```C++
|
||||
filter |= IdAndFlags::PUBLIC;
|
||||
```
|
||||
|
||||
</div>
|
||||
<div>
|
||||
|
||||
```alloy
|
||||
addBitfieldFlag[filterNow, filterNext, Public]
|
||||
```
|
||||
|
||||
</div>
|
||||
</div>
|
||||
|
||||
This might remind you of [Hoare Logic](https://en.wikipedia.org/wiki/Hoare_logic), where statements like:
|
||||
|
||||
$$
|
||||
\{ P \} \; s \; \{ Q \}
|
||||
$$
|
||||
|
||||
Read as:
|
||||
|
||||
> If $P$ is true before executing $s$, then $Q$ will be true after executing $s$.
|
||||
|
||||
$$
|
||||
\{ \text{filter} = \text{filterNow} \} \; \texttt{filter |= PUBLIC} \; \{ \text{filter} = \text{filterNext} \}
|
||||
$$
|
||||
|
||||
---
|
||||
|
||||
# Modeling Possible Searches
|
||||
|
||||
To combine several statements, we make it so that the "next" state of one statement is the "current" state of the next statement.
|
||||
|
||||
<div class="side-by-side">
|
||||
<div>
|
||||
|
||||
```C++
|
||||
curFilter |= IdAndFlags::PUBLIC;
|
||||
curFilter |= IdAndFlags::METHOD_FIELD;
|
||||
```
|
||||
|
||||
</div>
|
||||
<div>
|
||||
|
||||
```alloy
|
||||
addBitfieldFlag[filterNow, filterNext1, Public]
|
||||
addBitfieldFlag[filterNext1, filterNext2, Method]
|
||||
```
|
||||
|
||||
</div>
|
||||
</div>
|
||||
|
||||
This is reminiscent of sequencing Hoare triples:
|
||||
|
||||
$$
|
||||
\{ P \} \; s_1 \; \{ Q \} \; s_2 \; \{ R \}
|
||||
$$
|
||||
|
||||
---
|
||||
|
||||
# Modeling Possible Searches
|
||||
|
||||
Finally, if C++ code has conditionals, we need to allow for the possibility of either branch being taken. We do this by using "or" on descriptions of the next state.
|
||||
|
||||
<div class="side-by-side">
|
||||
<div>
|
||||
|
||||
```C++
|
||||
if (skipPrivateVisibilities) {
|
||||
curFilter |= IdAndFlags::PUBLIC;
|
||||
}
|
||||
|
||||
if (!includeMethods && receiverScopes.empty()) {
|
||||
curFilter |= IdAndFlags::NOT_METHOD;
|
||||
}
|
||||
```
|
||||
</div>
|
||||
<div>
|
||||
|
||||
```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]
|
||||
```
|
||||
</div>
|
||||
</div>
|
||||
|
||||
Putting this into a predicate, `possibleState`, we encode what searches the compiler can undertake.
|
||||
|
||||
**Takeaway**: We encoded the logic that configures possible searches in Alloy. This instructs the analyzer about possible cases to consider.
|
||||
|
||||
---
|
||||
|
||||
# Are there any bugs?
|
||||
|
||||
Model checkers ensure that all properties we want to hold, do hold. To find a counter example, we ask it to prove the negation of what we want.
|
||||
|
||||
```C
|
||||
wontFindNeeded: run {
|
||||
all searchState: SearchState {
|
||||
eventually some props: Props, fs: FilterState, fsBroken: FilterState {
|
||||
// Some search (fs) will cause a transition / modification of the search state...
|
||||
configureState[fs]
|
||||
updateOrSet[searchState.previousFilter, fs]
|
||||
// Such that a later, valid search... (fsBroken)
|
||||
configureState[fsBroken]
|
||||
|
||||
// Will allow for a set of properties...
|
||||
// ... that are left out of the original search...
|
||||
not bitfieldMatchesProperties[searchState.previousFilter, props]
|
||||
// ... and out of the current search
|
||||
not (bitfieldMatchesProperties[fs.include, props] and not bitfieldMatchesProperties[searchState.previousFilter, props])
|
||||
// But would be matched by the broken search...
|
||||
bitfieldMatchesProperties[fsBroken.include, props]
|
||||
// ... to not be matched by a search with the new state:
|
||||
not (bitfieldMatchesProperties[fsBroken.include, props] and not bitfieldOrNotSetMatchesProperties[searchState.previousFilter', props])
|
||||
}
|
||||
}
|
||||
}
|
||||
```
|
||||
|
||||
---
|
||||
# Uh-Oh!
|
||||
|
||||
|
||||
|
||||
---
|
||||
# The Bug
|
||||
|
||||
|
||||
|
||||
We need some gymnastics to figure out what variables make this model possible.
|
||||
|
||||
Alloy has a nice visualizer, but it has a lot of information.
|
||||
|
||||
In the interest of time, I found:
|
||||
|
||||
* If the compiler searches a scope first for `PUBLIC` symbols, ...
|
||||
* ...then for `METHOD_OR_FIELD`, ...
|
||||
* ...then for any symbols, they will miss things!
|
||||
|
||||
---
|
||||
<style scoped>
|
||||
section {
|
||||
font-size: 20px;
|
||||
}
|
||||
</style>
|
||||
|
||||
# The Reproducer
|
||||
To trigger this sequence of searches, we needed a lot more gymnastics.
|
||||
|
||||
<div class="side-by-side">
|
||||
<div>
|
||||
|
||||
```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;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
```
|
||||
</div>
|
||||
<div>
|
||||
|
||||
* 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`.
|
||||
|
||||
</div>
|
||||
</div>
|
||||
|
||||
---
|
||||
|
||||
<!-- _class: lead -->
|
||||
# **Thank you!**
|
||||
|
||||
|
||||
|
||||
Read more
|
||||
|
||||
---
|
||||
|
||||
<!-- _class: lead -->
|
||||
# Extra Slides
|
||||
|
||||
---
|
||||
|
||||
# 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 scope lookup phase
|
||||
* This piece is used by the production Chapel compiler.
|
||||
|
||||
Moreover, the order of where to look matters: method calls are preferred
|
||||
over global functions, "nearer" functions are preferred over "farther" ones.
|
||||
|
||||
---
|
||||
|
||||
@@ -155,96 +522,6 @@ 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"
|
||||
|
||||
```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;
|
||||
}
|
||||
|
||||
if (onlyMethodsFields) {
|
||||
filter |= IdAndFlags::METHOD_FIELD;
|
||||
|
||||
} 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...
|
||||
|
||||
---
|
||||
|
||||
<!-- _class: lead -->
|
||||
# Formal Methods
|
||||
|
||||
---
|
||||
# Types of Formal Methods
|
||||
|
||||
- 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.
|
||||
- Theorem proving is a heavier weight approach that involves building a formal proof of correctness.
|
||||
- Coq and Isabelle are examples of theorem provers.
|
||||
---
|
||||
<style scoped>
|
||||
li:nth-child(2) { color: lightgrey; }
|
||||
</style>
|
||||
# Types of Formal Methods
|
||||
|
||||
- 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.
|
||||
- Theorem proving is a heavier weight approach that involves building a formal proof of correctness.
|
||||
- Coq and Isabelle are examples of theorem provers.
|
||||
|
||||
|
||||
|
||||
**Reason**: I was in the middle of developing compiler code. I wanted to sketch
|
||||
the assumptions I was making and see if they held up.
|
||||
|
||||
---
|
||||
|
||||
# A Primer on Logic
|
||||
|
||||
Model checkers like Alloy are rooted in temporal logic, which builds on
|
||||
@@ -263,40 +540,6 @@ first-order logic. This includes:
|
||||
|
||||
---
|
||||
|
||||
# A Primer on Logic (example)
|
||||
|
||||
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.
|
||||
- $\Diamond p$ (in Alloy: `eventually p`) : A statement that will be true at some point in the future.
|
||||
|
||||
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;
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
# A Primer on Temporal Logic (example)
|
||||
|
||||
Some examples:
|
||||
@@ -387,131 +630,6 @@ pred bitfieldEqual[b1: Bitfield, b2: Bitfield] {
|
||||
|
||||
---
|
||||
|
||||
# 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.
|
||||
|
||||
<div class="side-by-side">
|
||||
<div>
|
||||
|
||||
```C++
|
||||
filter |= IdAndFlags::PUBLIC;
|
||||
```
|
||||
|
||||
</div>
|
||||
<div>
|
||||
|
||||
```alloy
|
||||
addBitfieldFlag[filterNow, filterNext, Public]
|
||||
```
|
||||
|
||||
</div>
|
||||
</div>
|
||||
|
||||
This might remind you of [Hoare Logic](https://en.wikipedia.org/wiki/Hoare_logic), where statements like:
|
||||
|
||||
$$
|
||||
\{ P \} \; s \; \{ Q \}
|
||||
$$
|
||||
|
||||
Read as:
|
||||
|
||||
> If $P$ is true before executing $s$, then $Q$ will be true after executing $s$.
|
||||
|
||||
$$
|
||||
\{ \text{filter} = \text{filterNow} \} \; \texttt{filter |= PUBLIC} \; \{ \text{filter} = \text{filterNext} \}
|
||||
$$
|
||||
|
||||
---
|
||||
|
||||
# Modeling Possible Searches
|
||||
|
||||
To combine several statements, we make it so that the "next" state of one statement is the "current" state of the next statement.
|
||||
|
||||
<div class="side-by-side">
|
||||
<div>
|
||||
|
||||
```C++
|
||||
curFilter |= IdAndFlags::PUBLIC;
|
||||
curFilter |= IdAndFlags::METHOD_FIELD;
|
||||
```
|
||||
|
||||
</div>
|
||||
<div>
|
||||
|
||||
```alloy
|
||||
addBitfieldFlag[filterNow, filterNext1, Public]
|
||||
addBitfieldFlag[filterNext1, filterNext2, Method]
|
||||
```
|
||||
|
||||
</div>
|
||||
</div>
|
||||
|
||||
This is reminiscent of sequencing Hoare triples:
|
||||
|
||||
$$
|
||||
\{ P \} \; s_1 \; \{ Q \} \; s_2 \; \{ R \}
|
||||
$$
|
||||
|
||||
---
|
||||
|
||||
# Modeling Possible Searches
|
||||
|
||||
Finally, if C++ code has conditionals, we need to allow for the possibility of either branch being taken. We do this by using "or" on descriptions of the next state.
|
||||
|
||||
<div class="side-by-side">
|
||||
<div>
|
||||
|
||||
```C++
|
||||
if (skipPrivateVisibilities) {
|
||||
curFilter |= IdAndFlags::PUBLIC;
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
if (onlyMethodsFields) {
|
||||
curFilter |= IdAndFlags::METHOD_FIELD;
|
||||
} else if (!includeMethods && receiverScopes.empty()) {
|
||||
curFilter |= IdAndFlags::NOT_METHOD;
|
||||
}
|
||||
|
||||
|
||||
|
||||
```
|
||||
</div>
|
||||
<div>
|
||||
|
||||
```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]
|
||||
```
|
||||
</div>
|
||||
</div>
|
||||
|
||||
Putting this into a predicate, `possibleState`, we encode what searches the compiler can undertake.
|
||||
|
||||
**Takeaway**: We encoded the logic that configures possible searches in Alloy. This instructs the analyzer about possible cases to consider.
|
||||
|
||||
---
|
||||
|
||||
# Modeling `previousFilter`
|
||||
|
||||
So far, all we've done is encoded what queries the compiler might make about a scope.
|
||||
@@ -531,6 +649,55 @@ one sig SearchState {
|
||||
|
||||
Above, `+` is used for union. `previousFilter` can either be a `Bitfield` or `NotSet`.
|
||||
|
||||
---
|
||||
# Types of Formal Methods
|
||||
|
||||
- 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.
|
||||
- Theorem proving is a heavier weight approach that involves building a formal proof of correctness.
|
||||
- Coq and Isabelle are examples of theorem provers.
|
||||
---
|
||||
<style scoped>
|
||||
li:nth-child(2) { color: lightgrey; }
|
||||
</style>
|
||||
# Types of Formal Methods
|
||||
|
||||
- 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.
|
||||
- Theorem proving is a heavier weight approach that involves building a formal proof of correctness.
|
||||
- Coq and Isabelle are examples of theorem provers.
|
||||
|
||||
|
||||
|
||||
**Reason**: I was in the middle of developing compiler code. I wanted to sketch
|
||||
the assumptions I was making and see if they held up.
|
||||
|
||||
---
|
||||
|
||||
# Putting it Together
|
||||
|
||||
We now have a model of what our C++ program is doing: it computes some set of filter flags, then runs a search, excluding the previous flags. It then updates the previous flags with the current search. We can encode this as follows:
|
||||
|
||||
```
|
||||
fact step {
|
||||
always {
|
||||
// Model that a new doLookupInScope could've occurred, with any combination of flags.
|
||||
all searchState: SearchState {
|
||||
some fs: FilterState {
|
||||
// This is a possible combination of lookup flags
|
||||
possibleState[fs]
|
||||
|
||||
// If a search has been performed before, take the intersection; otherwise,
|
||||
// just insert the current filter flags.
|
||||
updateOrSet[searchState.previousFilter, fs]
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
# Modeling `previousFilter`
|
||||
@@ -566,120 +733,3 @@ Otherwise, we set `previousFilter` to the intersection of `filter` and `previous
|
||||
|
||||
</div>
|
||||
</div>
|
||||
|
||||
---
|
||||
|
||||
# Putting it Together
|
||||
|
||||
We now have a model of what our C++ program is doing: it computes some set of filter flags, then runs a search, excluding the previous flags. It then updates the previous flags with the current search. We can encode
|
||||
this as follows:
|
||||
|
||||
```
|
||||
fact step {
|
||||
always {
|
||||
// Model that a new doLookupInScope could've occurred, with any combination of flags.
|
||||
all searchState: SearchState {
|
||||
some fs: FilterState {
|
||||
// This is a possible combination of lookup flags
|
||||
possibleState[fs]
|
||||
|
||||
// If a search has been performed before, take the intersection; otherwise,
|
||||
// just insert the current filter flags.
|
||||
updateOrSet[searchState.previousFilter, fs]
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
```
|
||||
|
||||
---
|
||||
# Are there any bugs?
|
||||
|
||||
Model checkers ensure that all properties we want to hold, do hold. To find a counter example, we ask it to prove the negation of what we want.
|
||||
|
||||
```C
|
||||
wontFindNeeded: run {
|
||||
all searchState: SearchState {
|
||||
eventually some props: Props, fs: FilterState, fsBroken: FilterState {
|
||||
// Some search (fs) will cause a transition / modification of the search state...
|
||||
configureState[fs]
|
||||
updateOrSet[searchState.previousFilter, fs]
|
||||
// Such that a later, valid search... (fsBroken)
|
||||
configureState[fsBroken]
|
||||
|
||||
// Will allow for a set of properties...
|
||||
// ... that are left out of the original search...
|
||||
not bitfieldMatchesProperties[searchState.previousFilter, props]
|
||||
// ... and out of the current search
|
||||
not (bitfieldMatchesProperties[fs.include, props] and not bitfieldMatchesProperties[searchState.previousFilter, props])
|
||||
// But would be matched by the broken search...
|
||||
bitfieldMatchesProperties[fsBroken.include, props]
|
||||
// ... to not be matched by a search with the new state:
|
||||
not (bitfieldMatchesProperties[fsBroken.include, props] and not bitfieldOrNotSetMatchesProperties[searchState.previousFilter', props])
|
||||
}
|
||||
}
|
||||
}
|
||||
```
|
||||
|
||||
---
|
||||
# Uh-Oh!
|
||||
|
||||
|
||||
|
||||
---
|
||||
# The Bug
|
||||
|
||||
|
||||
|
||||
We need some gymnastics to figure out what variables make this model possible.
|
||||
|
||||
Alloy has a nice visualizer, but it has a lot of information.
|
||||
|
||||
In the interest of time, I found:
|
||||
|
||||
* If the compiler searches a scope first for `PUBLIC` symbols, ...
|
||||
* ...then for `METHOD_OR_FIELD`, ...
|
||||
* ...then for any symbols, they will miss things!
|
||||
|
||||
---
|
||||
<style scoped>
|
||||
section {
|
||||
font-size: 20px;
|
||||
}
|
||||
</style>
|
||||
|
||||
# The Reproducer
|
||||
To trigger this sequence of searches, we needed a lot more gymnastics.
|
||||
|
||||
<div class="side-by-side">
|
||||
<div>
|
||||
|
||||
```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;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
```
|
||||
</div>
|
||||
<div>
|
||||
|
||||
* 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`.
|
||||
|
||||
</div>
|
||||
</div>
|
||||
|
||||
Reference in New Issue
Block a user