Abstract Filinski and Griffin have independently succeeded in extending the formulae-as-types notion to deal with continuations. Whereas Griffin adopted control operators primitively, Filinski adopted the duality of functions to construct a symmetric lambda-calculus in which continuations are first-class objects. In this paper, we construct a typed lambda-calculus with first-class configurations consisting of expressions and continuations of the same types. Our calculus corresponds to a natural deduction based on Rumfitt’s bilateralism. Function types are represented as the implication and but-not connectives in intuitionistic and paraconsistent logics, respectively. Our calculus is not only logically consistent, but also computationally consistent. Our calculus with call-by-value and call-by-name strategies correspond to Wadler’s call-by-value and call-by-name dual calculi, respectively. Furthermore, we propose a notion of relaxed configurations, which loosely take expressions and continuations of different types. We confirm that the relaxedness defines control operators for delimited continuations.

Data independence of iterations of a loop statement in a partitioned global address space (PGAS) language is a sufficient condition to enable parallel processing of the loop iterations on distributed memories. However, checking data independence is generally difficult. In this paper, we propose the non-interference property of statements and design a sub-language of a directive-based PGAS language XcalableMP with a type system using the notion of vertex centricity. Although data independence and non-interference are generally mutually orthogonal, non-interference of a statement in the sub-language, which can be checked easily on the type system, implies data independence. We also implemented type checking on the Omni compiler for XcalableMP and confirmed the effectiveness of our approach using case studies of directive-based parallelization and temporal blocking optimization of stencil kernels.

Modern concurrent copying garbage collection (GC), in particular, real-time GC, uses fine-grained synchronizations with a mutator, which is the application program that mutates memory, when it moves objects in its copy phase. It resolves a data race using a concurrent copying protocol, which is implemented as interactions between the collector threads and the read and write barriers that the mutator threads execute. The behavioral effects of the concurrent copying protocol rely on the memory model of the CPUs and the programming languages in which the GC is implemented. It is difficult, however, to formally investigate the behavioral properties of concurrent copying protocols against various memory models. To address this problem, we studied the feasibility of the bounded model checking of concurrent copying protocols with memory models. We investigated a correctness-related behavioral property of copying protocols of various concurrent copying GC algorithms, including real-time GC Stopless, Clover, Chicken, Staccato, and Schism against six memory models, total store ordering (TSO), partial store ordering (PSO), relaxed memory ordering (RMO), and their variants, in addition to sequential consistency (SC) using bounded model checking. For each combination of a protocol and memory model, we conducted model checking with a model of a mutator. In this wide range of case studies, we found faults in two GC algorithms, one of which is relevant to the memory model. We fixed these faults with the great help of counterexamples. We also modified some protocols so that they work under some memory models weaker than those for which the original protocols were designed, and checked them using model checking. We believe that bounded model checking is a feasible approach to investigate behavioral properties of concurrent copying protocols under weak memory models.