Data Centers

A Linear Type System for Multicore Programming

Date Added: Jun 2009
Format: PDF

ATS is a recently developed functional programming language that supports both linear and dependent types. They formalize a type system capable of guaranteeing safe manipulation of resources on multicore machines and establish its soundness. Multicore Programming is used for the construction of concurrent multi-threaded programs that can run on machines with multiple cores. They first present a language L|| 0 with a simple linear type system, using it as a starting point to set up the basic machinery for further development. There is a special constant function thread-create for thread creation, which can be used to implement a function thread-create join for creating-joinable-threads. The functions thread create and thread create join do not take into account the availability of CPU resource. Compared to spawn and sync, parallel let-binding makes code cleaner and probably easier to understand. However, parallel let-binding is also less flexible. This paper concluded that combining programming with theorem-proving (as is done in ATS) yields a promising approach to the construction of safer and more reliable programs. This paper also underlines that the programmer can accurately describe resources and then rely on the type system of ATS to preclude them being misused. It also formalized a type system to support safe concurrent programming and proven its type soundness.