Assumption-Commitment Types for Resource Management in Virtually Timed Ambients

TL;DR

This paper presents a type system for managing resources in nested virtualization environments modeled by virtually timed ambients, ensuring resource guarantees and safety properties.

Contribution

It introduces a novel type system based on assumptions about external resources to guarantee internal resource provisioning in virtually timed ambients.

Findings

Proves subject reduction and progress for well-typed processes.

Ensures upper bounds on resource needs are maintained during process reduction.

Formalizes resource management in nested virtualization through a calculus.

Abstract

This paper introduces a type system for resource management in the context of nested virtualization. With nested virtualization, virtual machines compete with other processes for the resources of their host environment in order to provision their own processes, which could again be virtual machines. The calculus of virtually timed ambients formalizes such resource provisioning, extending the capabilities of mobile ambients to model the dynamic creation, migration, and destruction of virtual machines. The proposed type system uses assumptions about the outside of a virtually timed ambient to guarantee resource provisioning on the inside. We prove subject reduction and progress for well-typed virtually timed ambients, expressing that upper bounds on resource needs are preserved by reduction and that processes do not run out of resources.