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

Edit and publish Alloy article

Browse Source
This commit is contained in:
Danila Fedorin 2023-06-04 21:56:45 -07:00
parent 8a2e91e65e
commit 250884c7bc
2 changed files with 45 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -62,15 +62,15 @@ sig Symbol {
properties: set Property properties: set Property
} }
pred flagMatchesPropery[flag: Flag, property: Property] { pred flagMatchesProperty[flag: Flag, property: Property] {
(flag = Method and property = PMethod) or (flag = Method and property = PMethod) or
(flag = MethodOrField and (property = PMethod or property = PField)) or (flag = MethodOrField and (property = PMethod or property = PField)) or
(flag = Public and property = PPublic) (flag = Public and property = PPublic)
} }
pred bitfieldMatchesProperties[bitfield: Bitfield, symbol: Symbol] { pred bitfieldMatchesProperties[bitfield: Bitfield, symbol: Symbol] {
all flag: bitfield.positiveFlags | some property: symbol.properties | flagMatchesPropery[flag, property] all flag: bitfield.positiveFlags | some property: symbol.properties | flagMatchesProperty[flag, property]
all flag: bitfield.negativeFlags | no property: symbol.properties | flagMatchesPropery[flag, property] all flag: bitfield.negativeFlags | no property: symbol.properties | flagMatchesProperty[flag, property]
} }
bitfieldExists: run { bitfieldExists: run {

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

@ -1,9 +1,8 @@
--- ---
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-06-04T21:56:00-07:00
tags: ["Compilers", "Alloy"] tags: ["Compilers", "Alloy"]
description: "In this post, I apply Alloy to a piece of code in the Chapel compiler to find a bug." description: "In this post, I apply Alloy to a piece of code in the Chapel compiler to find a bug."
draft: true
--- ---
__Disclaimer:__ though "my compiler code" makes for a fun title, I do not __Disclaimer:__ though "my compiler code" makes for a fun title, I do not
@ -26,7 +25,7 @@ fairly silly by the standards of "real" Alloy users.
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_,
which is the process of figuring out what each identifier, like `x`, refers to, which is the process of figuring out what each identifier, like `x`, refers to,
and what its type is. Even the first part of that is pretty complicated, what and what its type is. Even the first part of that is pretty complicated, what
with public and private variables, methods (which can be decalred outside with public and private variables, methods (which can be declared outside
of their receiver type in Chapel), and more... of their receiver type in Chapel), and more...
Scope resolution in Chapel is further complicated by the fact that the same Scope resolution in Chapel is further complicated by the fact that the same
@ -52,13 +51,34 @@ module M {
``` ```
If you don't know Chapel (and you probably don't!) this program already merits a fair If you don't know Chapel (and you probably don't!) this program already merits a fair
bit of explanation. A _module_ in Chapel (declared via a `module` keyword) bit of explanation. I've collapsed it for the sake of visual clarity; feel
free to expand the below section to learn more about the language features
used in the program above.
{{< details summary="Click here for an explanation of the above code snippet" >}}
A _module_ in Chapel (declared via a `module` keyword)
is just a collection of definitions. Such definitions could include variables, is just a collection of definitions. Such definitions could include variables,
methods, classes and more. Putting them in a module helps group them. methods, classes and more. Putting them in a module helps group them.
{{< todo >}} A _class_ in Chapel (declared via a `class` keyword) is much like a class in
Write the rest of this explanation. object oriented languages. The class `C` that we're creating on line 2 doesn't
{{< /todo >}} have any fields or methods -- at least not yet. We will, however, add methods
to it using Chapel's _secondary method_ mechanism (more on that in a moment).
The `proc` keyword is used to create functions and methods. On line 5, we
create a procedure called `foo` that does nothing. On line 8, because we
write `C.foo` instead of just `foo`, we're actually creating a method on
the class `C` we declared earlier. This method does nothing too. Notice
that although declaring classes in Chapel works about the same as declaring
classes in other languages, it's fairly unusual to be able to declare a
class method (like the `foo` on line 8 in this case) outside of the `class
C { ... }` section of code. This is part of the reason that Chapel method
resolution is complicated (methods can be declared anywhere!). The only
other language that I know of that supports this feature is Kotlin with its
[extension function
mechanism](https://kotlinlang.org/docs/extensions.html), but it's possible
that other languages have similar functionality.
{{< /details >}}
The interesting part of the snippet is the body of the `doSomething` method. The interesting part of the snippet is the body of the `doSomething` method.
It has a call to `foo`: but which `foo` is it referring to? There are two: It has a call to `foo`: but which `foo` is it referring to? There are two:
@ -87,10 +107,10 @@ the search order will be as follows:
be the non-method `foo`. be the non-method `foo`.
Notice that we've already had to search the module `M` twice, looking for Notice that we've already had to search the module `M` twice, looking for
different things each time. First, we were looking for only method, but different things each time. First, we were looking for only methods, but
later, we were looking for anything. However, this isn't as complicated as later, we were looking for anything. However, this isn't as complicated as
things can get. The simplifying aspect of this program is that both `doSomething` things can get. The simplifying aspect of this program is that both `doSomething`
and `C` are defined inside the class `C`, and therefore have access to its and `C` are defined inside the module `M`, and therefore have access to its
private methods and procedures. If we extracted `C.doSomething` into its private methods and procedures. If we extracted `C.doSomething` into its
own separate module, the program would look like this. own separate module, the program would look like this.
@ -119,7 +139,7 @@ Since `doSomething` is now in another module, it can't just access the `foo`s fr
and make use of them. I opted for a `use` statement, which, in its simplest form, and make use of them. I opted for a `use` statement, which, in its simplest form,
just brings all the declarations inside the `use`d module into the current scope. Thus, just brings all the declarations inside the `use`d module into the current scope. Thus,
the `use` statement on line 11 would bring all things declared in `M1` into the `use` statement on line 11 would bring all things declared in `M1` into
the scope inside `M2`. There's a catch, though: since `M2` is not declared the scope inside `M2`. There's a catch, though. Since `M2` is not declared
inside `M1`, a `use` statement will not be able to bring in _private_ symbols inside `M1`, a `use` statement will not be able to bring in _private_ symbols
from `M1` (they're private for a reason!). So, this time, when searching the scope from `M1` (they're private for a reason!). So, this time, when searching the scope
for `M1`, we will have to search only for public symbols. That's another, for `M1`, we will have to search only for public symbols. That's another,
@ -129,14 +149,13 @@ different way of searching `M1`. So far, we've seen three:
* Search `M1` for methods only. * Search `M1` for methods only.
* Search `M1` for public symbols only. * Search `M1` for public symbols only.
In Dyno, there are even more different ways of searching a single scope, and Dyno introduces more ways to search within a scope, including combinations of
some of them are mixes of others (one might consider, for instance, searching search types, such as looking only for public methods. To represent the various
for only public methods). To represent the various search configurations, search configurations, the Dyno team came up with using a bitfield of _flags_,
the Dyno team came up with using a bitfield of _flags_, each of which indicated each of which indicated a necessary condition for a symbol to be returned. A
a necessary condition for a symbol to be returned. A bitfield with flags set bitfield with flags set for two properties (like "public" and "method") requires
for two properties (like "public" and "method") requires that both such that both such properties be found on each symbol that's returned from a scope.
properties be found on each symbol that's returned from a scope. This led to This led to C++ code along the lines of:
C++ code along the lines of:
```C++ ```C++
auto allPublicSymbols = Flags::PUBLIC; auto allPublicSymbols = Flags::PUBLIC;
@ -167,7 +186,7 @@ In Dyno, we like to avoid additional work when we can. To do so, we track
which scopes have already been searched, and avoid searching them again. which scopes have already been searched, and avoid searching them again.
Since what comes up from a search depends on the flags, we store the flags Since what comes up from a search depends on the flags, we store the flags
alongside the scopes we've checked. __If we find that the previously-checked alongside the scopes we've checked. __If we find that the previously-checked
bitfield is a subset of the current biset, we just skip the search__. bitfield is a subset of the current bitset, we just skip the search__.
But then, what if it _isn't_ a subset? Another concern here is avoiding But then, what if it _isn't_ a subset? Another concern here is avoiding
duplicate results (it's easier to check for duplicate definitions if you duplicate results (it's easier to check for duplicate definitions if you
@ -186,7 +205,7 @@ versions of each flag available. Can't you just add those to the filter?
{{< message "answer" "Daniel" >}} {{< message "answer" "Daniel" >}}
Good question. The difference is a little bit tricky. If we just negated Good question. The difference is a little bit tricky. If we just negated
each flag, we'd turn an expression like \(A \land B\) into \(\lnot A \land each flag, we'd turn an expression like \(A \land B\) into \(\lnot A \land
\lnot B\). However, according to De Morgan's laws, the proper negation of \lnot B\). However, according to [De Morgan's laws](https://en.wikipedia.org/wiki/De_Morgan%27s_laws), the proper negation of
\(A \land B\) is \(\lnot A \lor \lnot B\) (notice the use of "or" instead \(A \land B\) is \(\lnot A \lor \lnot B\) (notice the use of "or" instead
of "and"). On the other hand, using an "exclude" bitfield negates the whole of "and"). On the other hand, using an "exclude" bitfield negates the whole
conjunction, rather than the individual flags, and so gives us the result conjunction, rather than the individual flags, and so gives us the result
@ -303,7 +322,7 @@ Here's the Alloy definition for everything I just said:
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 59 63 >}} {{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 59 63 >}}
Now, we can specify how flags in a bitfield relates to properties on a Now, we can specify how flags in a bitfield relate to properties on a
symbol. We can do so by saying which flags match which properties. The symbol. We can do so by saying which flags match which properties. The
`Method` flag, for instance, will be satisfied by the `PMethod` property. `Method` flag, for instance, will be satisfied by the `PMethod` property.
The `MethodOrField` flag is more lenient, and will be satisfied by either The `MethodOrField` flag is more lenient, and will be satisfied by either
@ -321,9 +340,9 @@ informally, the condition for a bitfield matching a symbol is twofold:
property on the symbol (that is to say, if `Method` is in the negative property on the symbol (that is to say, if `Method` is in the negative
flags set, then the symbol must not have `PMethod` property). It is more flags set, then the symbol must not have `PMethod` property). It is more
conveniently to formulate this -- equivalently -- as follows: for each conveniently to formulate this -- equivalently -- as follows: for each
negative flag, there most not be a property that satisfies it. negative flag, there must not be a property that satisfies it.
Each of the above two conditions translate quite literally into Alloy: Each of the above two conditions translates quite literally into Alloy:
{{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 71 74 >}} {{< codelines "Alloy" "dyno-alloy/DynoAlloy.als" 71 74 >}}