23 lines
1.4 KiB
Plaintext
23 lines
1.4 KiB
Plaintext
Formal methods are a set of techniques that are used to validate the correctness
|
||
of software. A particular category of these methods, model checking, uses the
|
||
mathematical language of temporal logic to construct specifications of software’s
|
||
behavior. A solver can then validate the constraints described in the formal
|
||
language and ensure that undesirable states do not occur.
|
||
|
||
This talk will be an experience report of using formal methods, specifically
|
||
the Alloy analyzer, to detect a bug in Chapel’s ‘Dyno’ compiler front-end library.
|
||
The area in which the bug was discovered is currently used in production, as
|
||
well as a part of editor tools such as chplcheck and chpl-language-server.
|
||
|
||
Specifically, Alloy was used to construct a formal specification of a part of
|
||
Chapel’s use/import lookup algorithm. Chapel has a number of complicated scoping
|
||
rules and possible edge cases in this area. By running this specification against
|
||
a solver, a sequence of steps was discovered that could cause the algorithm to
|
||
malfunction and produce incorrect results. A program that causes these steps to
|
||
occur was constructed and served as a concrete reproducer for the bug. This
|
||
reproducer was used to adjust the logic and fix the bug.
|
||
|
||
This talk will cover the fundamentals of temporal logic required for formal
|
||
specifications, the necessary parts of Chapel’s use/import lookup algorithm,
|
||
and the steps taken to encode and validate the compiler’s behavior.
|