Campus Event Calendar
Event Entry
What and Who
Address Spaces and Virtual Memory – Specification, Implementation, and Correctness
Mark Hillebrand
Promotionskolloquium
AG 1, AG 2, AG 3, AG 4, AG 5
AG Audience
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 13 June 2005
16:00
-- Not specified --
45
HS 001
Saarbrücken
Abstract
In modern operating systems tasks operate concurrently on a shared
logical memory under control of their address spaces. In the
implementation, the logical memory and address spaces are emulated with
main and swap memory, and address translation mechanism, and an
appropriate page fault handler, which is a (low-level) part of the
operating system implementation.This construction is correct if it is
transparent to the tasks. The formalization of this correctness
criterion is called a virtual memory simulation theorem.
In this thesis, such a theorem for an abstract multiprocessor is
formulated and proved. The theorem is applied to a concrete
hardware-software-implementation, the VAMP [BJKLPO3] extended with a
single-level address translation mechanism and an exemplary page fault
handler. It is shown how to extend the architecture and proofs to
support TLBs, multi-level translation, and multiprocessing.
logical memory under control of their address spaces. In the
implementation, the logical memory and address spaces are emulated with
main and swap memory, and address translation mechanism, and an
appropriate page fault handler, which is a (low-level) part of the
operating system implementation.This construction is correct if it is
transparent to the tasks. The formalization of this correctness
criterion is called a virtual memory simulation theorem.
In this thesis, such a theorem for an abstract multiprocessor is
formulated and proved. The theorem is applied to a concrete
hardware-software-implementation, the VAMP [BJKLPO3] extended with a
single-level address translation mechanism and an exemplary page fault
handler. It is shown how to extend the architecture and proofs to
support TLBs, multi-level translation, and multiprocessing.
Contact
--email hidden
passcode not visible
logged in users only
Bahareh Kadkhodazadeh, 06/07/2005 13:02 -- Created document.