Treffer: A Proof System for a PGAS Language.

Due to advances in hardware architectures such as multi-core/multi-threaded architectures, various refinements of the parallel programming models such as distributed shared space, global address space and partitioned global address space (PGAS) etc., are widely prevalent in programming languages designed for high performance computing. In this paper, we shall discuss a preliminary work on a proof system for such a language. The language referred to as PGAS<subscript>0</subscript>, is essentially an object-oriented language with features such as statically fixed set of places, asynchronous creation of activities, futures, atomics for synchronization etc. Many of the features of PGAS<subscript>0</subscript> are taken from the new experimental language X10 (built around Java) under design at IBM. The language distinguishes between local and remote data access with reference to threads. The atomic is the only construct that can be used for synchronization in PGAS<subscript>0</subscript> and is executed in a mutually exclusive manner at a place. One of the main safety properties of a PGAS<subscript>0</subscript> program is that a thread should not access non-local data object directly by dereferencing but use the construct future to obtain remote data. We shall describe the semantics of PGAS<subscript>0</subscript> and illustrate a proof system for the same with the motivation of establishing locality of data (an extremely useful from performance perspective). Further, we show how the same proof system can be used for establishing other concurrency properties. [ABSTRACT FROM AUTHOR]

Copyright of Concurrency, Compositionality & Correctness is the property of Springer Nature / Books and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)