Smit, A. (2001) Verifying a barrier algorithm with a mechanical theorem prover. Master's Thesis / Essay, Computing Science.
|
Text
Infor_Ma_2001_ASmit.CV.pdf - Published Version Download (1MB) | Preview |
Abstract
A way to reduce the execution time of a program, is to distribute the tasks of the program over several processors. It is not easy to design these programs because there are many factors you have to take into account, like deadlock (tasks are waiting for each other) or the possibility that tasks come in a infinite loop. To prove such a program's correctness is very complex. It is not recommendable to prove such a program by hand. A lot of administration is needed for all the different cases the program can go into during its execution. Also is it very time consuming and the chance of overlooking something or making a mistake is very high. An approach to prove the correctness of such a complex program is the use of a mechanical theorem prover. A mechanical theorem prover is a piece a software that does the proving for the designer. Learning how such a prover works can be very hard. The assignment was to verify a barrier algorithm with such a theorem prover and will be discussed in this paper. The goal of this assignment is to learn more about mechanical theorem provers. But also how it is to be working independently on such a theoretical problem like this.In chapter 2 we will lay out the theory that is needed to understand a concurrent program like the barrier. The barrier itself is also discussed in this chapter including a global proof. In chapter 3 we will discuss some aspects of theorem provers. Aspects like what they are and what they do, and also the advantages and disadvantages of theorem provers. We will conclude that chapter with some information about how to use the theorem prover NQTHM cf. [4] and why we have chosen this particular theorem prover for this assignment. In chapter 4 and 5 we give our implementation of the barrier in NQTHM code. In chapter 4 the implementation of the prelude we use for the barrier implementation is discussed and the barrier itself is layed out in chapter 5.Chapter 6 contains all the problems and obstacles we encountered during the proof. In chapter 7 we will discuss extensions that can be made to the barrier algorithm. We conclude this paper with concluding remarks.
| Item Type: | Thesis (Master's Thesis / Essay) |
|---|---|
| Degree programme: | Computing Science |
| Thesis type: | Master's Thesis / Essay |
| Language: | English |
| Date Deposited: | 15 Feb 2018 07:29 |
| Last Modified: | 15 Feb 2018 07:29 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/8847 |
Actions (login required)
 |
View Item |