COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |
University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Decoding Nets: A Formal Take on Address Translation
Decoding Nets: A Formal Take on Address TranslationAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Jamie Vicary. This talk has been canceled/deleted Modern computing hardware is enormously complicated: a single memory request traverses multiple hardware translation and caching steps until it reaches its intended destination, which often appears at different physical addresses for different requesters. Correctly capturing the complexity of this process is essential for correct system operation and system verification. We introduce decoding nets, a formal description for memory and interrupt systems, which we have successfully used in practice for page table generation, memory management and interrupt controller configuration. Furthermore, we are actively using them to verify isolation guarantees of the ARM confidential compute architecture. This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. This talk is included in these lists:This talk is not included in any other list Note that ex-directory lists are not shown. |
Other listsPublic Understanding of Risk Clark Lectures BCbD Annual Lecture 2021Other talksString scattering and generalized automorphic forms III Ecosystem: BedRock Immunotherapy: A piece of the puzzle for treating brain cancer Cambridge - Nova Workshop - Day 1 Coffee in Battcock F17 - Introductions Predicting Transitions far from Equilibrium |