FORMAL DERIVATION OF LAMPORT’S BAKERY ALGORITHM IN MULTIPROGRAMMING

LEWU, RETZI YOSIA and Pinontoan, Benny (2004) FORMAL DERIVATION OF LAMPORT’S BAKERY ALGORITHM IN MULTIPROGRAMMING. Skripsi thesis, UNIVERSITAS KATOLIK DE LA SALLE.

	PDF COVER-DAFTAR_ISI_RetziLewu.pdf Download (682kB)
	PDF BAB_ISI-LAMPIRAN_RetziLewu.pdf Restricted to Repository staff only Download (692kB)

Official URL: http://digilib.unikadelasalle.ac.id/

Abstract

Algorithm is a step-by-step procedure to solve certain problem. It is later transformed into another form that is understandable for computer, called program. In designing an algorithm there are two things needed. They are efficiency and correctness. Program correctness is important since a program will be useless if it cannot perform an expected output. On the other side, efficiency is also important. In sequential programs, the statement is executed one after another. Meanwhile, there are some sections of that program that can be synchronized so that they can be executed simultaneously. Nevertheless, the synchronization process needs some rules or protocols so that they will do exactly the same as they were put sequentially. The big advantage here is the efficiency and it is the main issue of multiprogramming. The synchronized programs are called a multiprogram.
A problem may occur when those program are being synchronized. For example, in a problem named mutual Exclusion Problem, there are two component trying to enter critical section. A solution of this problem must ensure that the mutual exclusion property is satisfied and guarantee that there is no deadlock.
The subject concerned in this thesis, shows how the derivation of Lamport’s Bakery Algorithm to solve the mutual exclusion problem is made simultaneously with its proof of correctness, both locally and globally. This work is done through the approximation method by using the Gries-Owicki Theorem and some logic and calculus. The approximation is done repeatedly to find a final solution that satisfies the given specification.

Keywords: efficiency, correctness, sequential program, synchronization, multiprogramming, multiprogram, The Gries-Owicki Theorem, local correctness, global correctness, Lamport’s Bakery Algorithm, Mutual Exclusion, deadlock.

Item Type:

Thesis (Skripsi)

Creators: