Web-Projects
/
blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Make some more progress on the Alloy article.

This commit is contained in:
Danila Fedorin 2023-05-14 16:00:55 -07:00
parent 9ae4798d80
commit 384f5de765
2 changed files with 298 additions and 47 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

55
code/dyno-alloy/DynoAlloy.als
View File

@ -10,8 +10,7 @@ sig Bitfield {
/* A filter state has filterFlags and excludeFlags, both represented as conjunctions. */
sig FilterState {
, include: Bitfield
, exclude: Bitfield
, curFilter: Bitfield
}
/* Initially, no search has happeneed for a scope, so its 'found' is not set to anything. */
@ -111,41 +110,43 @@ matchingBitfieldExists3: run {
}
}
pred configureState[filterState: FilterState] {
pred possibleState[filterState: FilterState] {
some initialState: FilterState {
// Each lookup in scope starts with empty filter and exclude flags
bitfieldEmpty[initialState.include] and bitfieldEmpty[initialState.exclude]
// Each lookup in scope starts with empty filter flags
bitfieldEmpty[initialState.curFilter]
// The intermediate states (bf1) are used for sequencing of operations.
some bf1 : Bitfield {
// The intermediate states (bitfieldMiddle) are used for sequencing of operations.
some bitfieldMiddle : Bitfield {
// Add "Public" depending on skipPrivateVisibilities
addBitfieldFlag[initialState.include, bf1, Public] or
bitfieldEqual[initialState.include, bf1]
addBitfieldFlag[initialState.curFilter, bitfieldMiddle, Public] or
bitfieldEqual[initialState.curFilter, bitfieldMiddle]
// If it's a method receiver, add method or field restriction
addBitfieldFlag[bf1, filterState.include, MethodOrField] or
addBitfieldFlag[bitfieldMiddle, filterState.curFilter, MethodOrField] or
// if it's not a receiver, filter to non-methods (could be overridden)
addBitfieldFlagNeg[bf1, filterState.include, Method] or
// Maybe methods are not being included but it's not a receiver, so no change.
bitfieldEqual[bf1, filterState.include]
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]
}
// Exclude filter doesn't change here
initialState.exclude = filterState.exclude
}
}
pred oldUpdate[toSet: Bitfield + NotSet, setTo: FilterState] {
toSet' in Bitfield and bitfieldIntersection[toSet, setTo.include, toSet']
possibleStateExists: run {
some filterState : FilterState | possibleState[filterState] and #filterState.curFilter.positiveFlags = 1
}
pred update[toSet: Bitfield + NotSet, setTo: FilterState] {
toSet' in Bitfield and bitfieldIntersection[toSet, setTo.curFilter, toSet']
}
pred newUpdate[toSet: Bitfield + NotSet, setTo: FilterState] {
(not bitfieldIncomparable[toSet, setTo.include] and oldUpdate[toSet, setTo]) or
(bitfieldIncomparable[toSet, setTo.include] and toSet = toSet')
(not bitfieldIncomparable[toSet, setTo.curFilter] and update[toSet, setTo]) or
(bitfieldIncomparable[toSet, setTo.curFilter] and toSet = toSet')
}
pred updateOrSet[toSet: Bitfield + NotSet, setTo: FilterState] {
(toSet in NotSet and toSet' = setTo.include) or
(toSet not in NotSet and oldUpdate[toSet, setTo])
(toSet in NotSet and toSet' = setTo.curFilter) or
(toSet not in NotSet and update[toSet, setTo])
}
pred excludeBitfield[found: Bitfield + NotSet, exclude: Bitfield] {
@ -163,7 +164,7 @@ fact step {
all searchState: SearchState {
some fs: FilterState {
// This is a possible combination of lookup flags
configureState[fs]
possibleState[fs]
// If a search has been performed before, take the intersection; otherwise,
// just insert the current filter flags.
@ -178,21 +179,21 @@ example: run {
// 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...
configureState[fs]
possibleState[fs]
updateOrSet[searchState.found, fs]
// Such that a later, valid search... (fsBroken)
configureState[fsBroken]
possibleState[fsBroken]
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.include, symbol] and not bitfieldMatchesProperties[searchState.found, symbol])
not (bitfieldMatchesProperties[fs.curFilter, symbol] and not bitfieldMatchesProperties[searchState.found, symbol])
// But would be matched by the broken search...
bitfieldMatchesProperties[fsBroken.include, symbol]
bitfieldMatchesProperties[fsBroken.curFilter, symbol]
// ... to not be matched by a search with the new state:
not (bitfieldMatchesProperties[fsBroken.include, symbol] and not bitfieldMatchesProperties[exclude, symbol])
not (bitfieldMatchesProperties[fsBroken.curFilter, symbol] and not bitfieldMatchesProperties[exclude, symbol])
}
}
}

290
content/blog/dyno_alloy/index.md
View File

@ -205,7 +205,7 @@ 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
touched Alloy before this, so be warned: this is what I came up with on my
own attempt.
### Modeling Flags and Bitsets in Alloy
@ -245,13 +245,13 @@ some condition holds for some arguments. This might seem abstract; as an
example, here's `bitfieldEmpty`, which checks that a bitfield has no flags
set.
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 27 29 >}}
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 26 28 >}}
The `#` operator in Alloy is used to check the size of a set. So, to check
if a bitfield is empty, I simply check if there are neither positive nor
negative flags. Probably the most unusual aspect of this piece of code is
that equality is written as `=`, as opposed to `==` like in most common
languages. This is because, like I said, alloy is all about relations and
languages. This is because, like I said, Alloy is all about relations and
predicates, and not at all about imperative manipulation of data. So,
there's no need to reserve `=` for assignment.
@ -259,7 +259,7 @@ The next step from here is a predicate that accepts two arguments,
`bitfieldEqual`. As its name suggests, this predicate accepts two
bitfields, and makes sure they have exactly the same flags set.
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 31 33 >}}
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 30 32 >}}
So far, this has been pretty similar to just writing boolean functions in a
language like C++. However, the similarity is only superficial. An easy way
@ -281,7 +281,7 @@ _does_ the output of a bitfield intersection connect to the two operands
being intersected? Well, its two flag sets will be intersections of the
flag sets of the inputs!
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 35 38 >}}
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 34 37 >}}
Next, let's talk about what flags _do_. They are used to include and
exclude symbols based on certain properties. One property is being a
@ -293,9 +293,9 @@ can have multiple properties (e.g., a public method). Unlike our bitfields,
though, we won't be modeling symbols as having both positive and negative
properties. That is to say, we won't have a "not public" property: the
absence of the "public" property will be enough to make something private.
Here's the alloy definition for everything I just said:
Here's the Alloy definition for everything I just said:
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 60 64 >}}
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 59 63 >}}
Now, we can specify how flags in a bitfield relates to properties on a
symbol. We can do so by saying which flags match which properties. The
@ -304,7 +304,7 @@ The `MethodOrField` flag is more lenient, and will be satisfied by either
`PMethod` or `PField`. Here's a predicate `flagMatchesProperty` that
encodes all the flag-property combinations:
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 66 70 >}}
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 65 69 >}}
A bitfield matching a symbol is a little bit more complicated. Said
informally, the condition for a bitfield matching a symbol is twofold:
@ -319,20 +319,20 @@ informally, the condition for a bitfield matching a symbol is twofold:
Each of the above two conditions translate quite literally into Alloy:
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 72 75 >}}
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 71 74 >}}
We can read line 73 as "for each flag in a bitfield's positive flags, there
must be some property in the symbol that matches it". Similarly, line 74
can be read out loud as "for each flag in the negative flags, no property
in the symbol must match it".
We've written a fair bit of alloy. If you're anything like me, you might be
We've written a fair bit of Alloy. If you're anything like me, you might be
getting a bit twitchy: how do we even check that any of this works? For
this, we'll need to run our model. We will give Alloy a claim, and ask
it to find a situation in which that claim holds true. The simplest claim
is "there exists a bitfield".
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 77 79 >}}
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 76 78 >}}
Executing this model yields a pretty interesting bitfield: one in which every single flag is set -- both the positive and negative versions.
@ -343,7 +343,7 @@ You can't be and not be a method at the same time, for instance. For for a
more interesting example, let's ask for a bitfield that matches some
symbol.
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 81 83 >}}
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 80 82 >}}
The output here is pretty interesting too. Alloy finds a symbol and a
bitfield that matches it, but they're both empty. In effect, it said:
@ -357,31 +357,31 @@ Let's try nudge it towards a more interesting case. I'm going to ask for a
filter with one positive and one negative flag, and a symbol with two
properties.
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 85 92 >}}
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 84 91 >}}
The results are more interesting this time: we get a filter for private
methods, and a private symbol that was... both a field and a method?
{{< figure src="matching_bitfield_exists_2.png" caption="Alloy's spiced up output satisfying \"a bit field that matches a symbol exists\"" >}}
We never told alloy that a symbol can't be both a field and a method. It
We never told Alloy that a symbol can't be both a field and a method. It
had no idea what the flags meant, just that they exist.
To let Alloy know what we do -- that the two properties are incompatible --
we can use a _fact_. To me, the most natural way of phrasing this is "there
is never a symbol that has both the method and field properties". Alas,
Alloy doesn't have a `never` keyword; it only has `always`. So I opt instead
for an alternative formulation: "there are always zero symbols that are
both methods and fields". In alloy, the claim looks like this:
both methods and fields". In Alloy, the claim looks like this:
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 94 99 >}}
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 93 98 >}}
Re-running the example program with this fact, alloy spits out a filter for
Re-running the example program with this fact, Alloy spits out a filter for
public non-method symbols, and a symbol that's a public field. Public
fields also aren't a thing in Chapel (all fields in a class are publicly
readable in the current version of the language). Perhaps it's time for
another fact.
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 100 104 >}}
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 99 103 >}}
But now, Alloy fails to come up with anything at all. That makes sense: by
restricting the search to a symbol with two properties, and making `PField`
@ -392,13 +392,255 @@ method, so making any of them negative would guarantee that our symbol
would not be found. Let's change the example up a bit to only ask for
positive flags.
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 106 112 >}}
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 105 111 >}}
This time, alloy gives us a symbol that's a public method, and a filter
This time, Alloy gives us a symbol that's a public method, and a filter
that only looks for public methods. Fair enough.
{{< figure src="matching_bitfield_exists_3.png" caption="Alloy's spiced up output satisfying \"a bit field that matches a symbol exists\"" >}}
### Exploring Possible Search Configurations
So now we have a descriptioin of filters and symbols in scopes. The next thing
on the itinerary is modeling how the filters (include and exclude) are
configured during scope search in Dyno. For this, let's take a look at the
C++ code in Dyno.
I'll be using the branch that I was working on at the time of trying to
apply Alloy. First, here's the code in C++ that defines the various flags
I'd be working with (though I've omitted flags that are not currently
used in the implementation).
```C++
enum {
/** Public */
PUBLIC = 1,
/** Not public (aka private) */
NOT_PUBLIC = 2,
/** A method or field declaration */
METHOD_FIELD = 4,
/** Something other than (a method or field declaration) */
NOT_METHOD_FIELD = 8,
/** A method declaration */
METHOD = 64,
/** Something other than a method declaration */
NOT_METHOD = 128,
};
```
These are the flags that we model using a `Bitset`: `PUBLIC`,
`METHOD_FIELD`, and `METHOD` are modeled using `positiveFlags`, and
`NOT_PUBLIC`, `NOT_METHOD_FIELD`, and `NOT_METHOD` are modeled using
`negativeFlags`. There are a lot of flags here, and it's not hard to
imagine that _some_ combination of these flags will cause problems in our
system (particularly when we _know_ it's an approximation). However, the
flags aren't used arbitrarily; in fact, it wasn't too hard to track down the
most important place in the code where bitsets are built.
```C++{linenos=true, linenostart=914}
IdAndFlags::Flags curFilter = 0;
/* ... some unrelated code ... */
if (skipPrivateVisibilities) {
curFilter |= IdAndFlags::PUBLIC;
}
if (onlyMethodsFields) {
curFilter |= IdAndFlags::METHOD_FIELD;
} else if (!includeMethods && receiverScopes.empty()) {
curFilter |= IdAndFlags::NOT_METHOD;
}
```
The above code converts the current search parameters into `Bitfield`
flags. For instance, if a `use` statement is being processed that doesn't
have access to private fields, `skipPrivateVisibilities` will be set.
On the other hand, if the calling code didn't explicitly ask for methods,
and if there's no method receiver, then the last condition will be true.
These various conditions are converted into bits and applied to
`curFilter`. Then, `curFilter` is used for looking up symbols in a scope.
It's not too hard to model this by just looking at the code, and
enumerating the possibilities. The first `if` statement can either be true
or false, and then the subsequent `if`-`else` chain creates three
possibilities in each case: either `METHOD_FIELD` is set, or `NOT_METHOD`,
or nothing.
However, I envisioned this condition to possibly grow in complexity as more
search configurations became necessary (in that, the `NOT_METHOD` option
was an addition in my new branch). I therefore chose to model the possible
`Bitfield` values more faithfully, by mimicking the imperative C++ code.
{{< dialog >}}
{{< message "question" "reader" >}}
Wait, something sounds off. Just earlier, you said Alloy "is not at all about
imperative manipulation of data". But now, we're going to mimic plain
imperative C++ code?
{{< /message >}}
{{< message "answer" "Daniel" >}}
Alloy the programming language is still not imperative. However, we can
<em>model</em> imperative behavior in Alloy. The way I see it, doing so
requires us to venture a tiny bit into the realm of <em>semantics</em>
for programming languages, in particular for imperative languages. This
"venture" is very minimal though, and you really don't need to know much
about semantics to understand it.
{{< /message >}}
{{< message "question" "reader" >}}
Alright. How does one model imperative behavior in Alloy?
{{< /message >}}
{{< message "answer" "Daniel" >}}
On to that next.
{{< /message >}}
{{< /dialog >}}
The essential piece of insight to modeling an imperative language, though
it sounds a little bit tautological, is that _statements are all about
manipulating state_. For example, state could be the value of a variable.
If you start with the variable `x` storing the number `6`, and then execute
the statement `x = x * 7`, the final value of `x` will be `42`. Thus, state
has changed. To put this in terms Alloy would understand -- relations and
sets -- a statement connects (relates) states before it's executed to states
after it's executed. In our particular example, the connection would
between the state `x = 6` and the state `x = 42`. In the case of adding the
`PUBLIC` to `curFilter`, as on line 917 in the above code block, we could
state the relationship as follows:
```Alloy
addBitfieldFlag[bitfieldBefore, bitfieldAfter, Public]
```
The above code states that `bitfieldAfter` (the state _after_ line 917) is
the same `Bitfield` as `bitfieldBefore` (the state _before_ line 917), except
that the `Public` flag has been added to it.
Things are a little more complicated when it comes to modeling the whole
`if`-statement on line 916. If we wanted to be very precise, we'd need to
encode the other variables (such as `skipPrivateVisibilities`), how they're
set, and what values are possible. However, for the sake of keeping the
scope of this model manageable for the time being, I'm content to do
something simpler -- that is, acknowledge that the code on line 917 may or
may not run. If it does run, our previous `addBitfieldFlag` will be the
correct restriction on the before and after states. However, if it doesn't,
the state shouldn't change at all. Therefore, we can model lines 916
through 918 as follows (notice the `or`):
```Alloy
addBitfieldFlag[bitfieldBefore, bitfieldAfter, Public] or
bitfieldEqual[bitfieldBefore, bitfieldAfter]
```
The next thing to note is that there are two `if` statements one after another.
The state "after" the first statement is one and the same as the state
"before" the second statement. Using arrows to represent the "before-after"
relationship created by each statement, we can visualize the whole
situation as follows:
{{< latex >}}
\text{initial state}
\xRightarrow{\text{first statement}}
\text{middle state}
\xRightarrow{\text{second statement}}
\text{final state}
{{< /latex >}}
We'll write our Alloy code to match:
```Alloy
/* First if statement */
addBitfieldFlag[bitfieldBefore, bitfieldMiddle, Public] or
bitfieldEqual[bitfieldBefore, bitfieldMiddle]
/* ... something connecting bitfieldMiddle and bitfieldAfter ... */
```
From here, we can handle the second `if`/`else` chain in the same way we
did the first `if`-statement: by making all three outcomes of the chain be
possible, and creating an `or` of all of them.
```Alloy
/* First if statement */
addBitfieldFlag[bitfieldBefore, bitfieldMiddle, Public] or
bitfieldEqual[bitfieldBefore, bitfieldMiddle]
/* Second if statement */
addBitfieldFlag[bitfieldMiddle, bitfieldAfter, MethodOrField] or
addBitfieldFlagNeg[bitfieldMiddle, bitfieldAfter, Method] or
bitfieldEqual[bitfieldMiddle, bitfieldAfter]
```
So that helps model the relevant Dyno code. However, what we really want is
an Alloy predicate that classifies possible outcomes of the piece of code:
is a particular combination of flags possible or not? Here's the piece of
Alloy that does so:
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 113 132 >}}
The `FilterState` on the first line (and elsewhere, really), is new. I'm
trying to be explicit about the state in this particular computation. Its
definition is very simple: currently, the only state we care about is the
`Bitfield` corresponding to `curFilter` in the C++ code above.
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 12 14 >}}
There's not much more to the predicate. It says, in English, that a state
`filterState` is possible if, starting from an empty initial state
`initialState`, the model of our C++ code can end up with its particular
set of flags in the `curFilter` bitfield.
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
when running subsequent searches.
Dyno implemented this roughly as follows:
1. It kept a mapping of (searched scope → search bitfield). Initially, this
mapping was empty.
2. When a scope was searched for the first time, its `curFilter` / search
bitfield was stored into the mapping.
3. When a scope was searched after that, the previously-stored flags in the
mapping were excluded (that's the \\(A\\land\\lnot B\\) behavior), and
the bitfield in the mapping was updated to be the intersection of
`curFilter` and the stored flags.
We'll simplify the model by doing away with the mapping, and considering
only a single scope that is searched many times. We'll represent the stored
flags as a field `found`, which will be one of two things: either a
`Bitfield` representing the previously-stored search configuration, or a
`NotSet` sentinel value, representing a scope that hasn't been searched
yet. The Alloy code:
{{< codelines "alloy" "dyno-alloy/dynoalloy.als" 21 23 >}}
The `NotSet` sentinel value is defined in a very simple way:
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 17 17 >}}
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"
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
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`.
{{< todo >}}
The rest of the article
{{< /todo >}}
@ -408,6 +650,14 @@ The rest of the article
This section is temporary
{{< /todo >}}
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:
a small-ish program to illustrate what I mean.
```Chapel