K Framework
K Framework is a tool for formally verifying programming languages and software / hardware systems.
Runtime Verification, the company behind K Framework, invited us to participate in developing the tool. Serokell's task was to improve the performance of the slow parts of the Haskell backend so that users could perform verification faster.
Verification
In software development, formal verification is the act of using formal methods to make sure that algorithms, software systems, or programming languages will work as intended by their creators.
It's usually done by creating a mathematical model of a project and then proving that it satisfies certain properties.
Formal verification enables programmers to create more reliable software, detect bugs early in the design, and uncover ambiguities.
In detail
K Framework enables developers to design and model programming languages and other software projects.
The main part of the framework is a programming and specification language called K. The framework provides tools for using specifications written in K to build such programs as interpreters, compilers, model checkers, etc.
We worked with the Haskell part of the framework to help Runtime Verification overcome multiple issues accumulated by the project owner in the backlog.
Our tasks included:
Improving the speed of the framework with Haskell code profiling and optimization.
Catching bugs, solving issues, and helping implement existing feature requests.
Our collaboration
Audit and optimization of Haskell backend code
At start, we were invited to audit, profile, and optimize the Haskell backend responsible for parsing and symbolic execution of the K language.
- We profiled the project's code with an automatic profiling tool that uncovers parts of code that take a lot of time to execute. In addition to that, we also did manual analysis of the code.
- Then, we worked to optimize the code through such techniques as inlining, specialization monomorphization, and other more specialized techniques.
- Each change to the Haskell backend of K Framework is evaluated using a set of regression tests. They are a part of the development process, and show how the introduced changes impact backend performance.
- Sequential test running required a lot of resources and time. In addition to our optimization work, we set up a Linux server that allows us to run parallel tests in closed environments.
As a result of our work, the time, required for completing tests, was decreased by up to 20%.
Closer work with K Framework
Our initial work laid the foundation for further collaboration on a new level that required deeper understanding of the product domain. Under certain conditions, the framework ran incorrectly – there were implementation issues.
Our task was to delve deeper into the internal logic of the framework and work with the client to discover the reasons behind them. We worked on multiple sub-issues to find the causes and fix each problematic area.
We were working closely with the K-Framework team, familiarizing ourselves with the framework to enable more autonomous work on the issues.
Conclusion
Developing verification software is a challenging task, as it requires solid mathematical logic knowledge and a mature approach to software development. With our expertise in similar projects and academic background, we were well-equipped to handle the project in a way that satisfies our client.