Sharing Analysis in the Pawns Compiler

TL;DR

This paper introduces sharing analysis techniques for the Pawns programming language, enabling safe encapsulation of impure effects like destructive updates while supporting advanced features such as pointers, higher-order functions, and explicit sharing controls.

Contribution

It presents a novel sharing analysis that handles explicit pointers, destructive updates, and higher-order functions with sharing constraints, enhancing safety and expressiveness in Pawns.

Findings

Sharing analysis effectively manages destructive updates and pointers.

The approach ensures safe encapsulation of impurity in pure functions.

It supports higher-order functions with sharing pre- and post-conditions.

Abstract

Pawns is a programming language under development that supports algebraic data types, polymorphism, higher order functions and "pure" declarative programming. It also supports impure imperative features including destructive update of shared data structures via pointers, allowing significantly increased efficiency for some operations. A novelty of Pawns is that all impure "effects" must be made obvious in the source code and they can be safely encapsulated in pure functions in a way that is checked by the compiler. Execution of a pure function can perform destructive updates on data structures that are local to or eventually returned from the function without risking modification of the data structures passed to the function. This paper describes the sharing analysis which allows impurity to be encapsulated. Aspects of the analysis are similar to other published work, but in addition it handles explicit pointers and destructive update, higher order functions including closures and pre- and post-conditions concerning sharing for functions.