Physical Adressing on Real Hardware in Isabelle/HOL
Lukas Humbel (home)
, 09 November 2018
Modern memory systems are much more complicated than the traditionally assumed
virtual and physical address space separation. We explain in this post which
effects can not solely expressed by the basic model and are important for
correct function of operating systems. We summarize our recent paper.
In this work we present a theory for addressing in such modern memory
subsystems. We formalize the theory in Isabelle/HOL.
A hammer you can only hold by the handle
Andrea Lattuada (@utaal)
, 05 November 2018
Today we’re looking at the rust borrow checker from a different perspective. As you may know, the borrow checker is designed to safely handle memory allocation and ownership, preventing accessess to invalid memory and ensuring data-race freedom. This is a form of resource management: the borrow checker is tracking who’s in charge of a chunk of memory, and who is currently allowed to read or write to it. In this post, we’ll see how these facilities can be used to enforce higher-level API constraints in your libraries and software. Once you’re familiar with these techniques, we’ll cover how the same principles apply to advanced memory management and handling of other more abstract resources.