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.
|