A Modality for Safe Resource Sharing and Code Reentrancy

Abstract. The potential of linear logic in facilitating reasoning on resource usage has long been recognized. However, convincing uses of linear types in practical programming are still rather rare. In this paper, we present a general design to effectively support practical programming with linear types. In particular, we introduce and then formalize a modality, which we refer to as the sharing modality, in support of sharing of linear resources (with no use of locks). We develop the underlying type theory for the sharing modality and establish its soundness based on a notion of types with effects. We also point out an intimate relation between this modality and the issue of code reentrancy. In addition, we present realistic examples to illustrate the use of sharing modality, which are verified in the programming language ATS and thus provide a solid proof of concept.

• Type: Journal
• Year: 2010
• Where: ICTAC
• Authors: Rui Shi, Dengping Zhu, Hongwei Xi
• Keywords: Applied Computing, ICTAC 2010, Linear, Linear Types, Sharing Modality