Santa Claus: Formal analysis of a process-oriented solution.

Welch, Peter H. and Pedersen, Jan B. (2010) Santa Claus: Formal analysis of a process-oriented solution. ACM Transactions on Programming Languages and Systems (TOPLAS), 32 (4). pp. 182-196. ISSN 0164-0925. (The full text of this publication is not available from this repository)

The full text of this publication is not available from this repository. (Contact us about this Publication)
Official URL
http://www.cs.kent.ac.uk/pubs/2010/3065

Abstract

With the commercial development of multicore processors, the challenges of writing multi-threaded programs to take advantage of these new hardware architectures are becoming more and more pertinent. Concurrent programming is necessary to achieve the performance that the hardware offers. Traditional approaches present concurrency as an advanced topic: they have proven difficult to use, reason about with confidence, and scale up to high levels of concurrency. This paper reviews process oriented design based on Hoare's algebra of Communicating Sequential Processes (CSP), and proposes that this approach to concurrency leads to solutions that are manageable by novice programmers -- that is, they are easy to design and maintain, that they are scalable for complexity, obviously correct and relatively easy to verify using formal reasoning and/or model checkers. These solutions can be developed in conventional programming languages (through CSP libraries) or specialised ones (such as occam-pi) in a manner that directly reflects their formal expression. Systems can be developed without needing specialist knowledge of the CSP formalism, since the supporting mathematics is burnt into the tools and languages supporting it. We illustrate these concepts with the Santa Claus Problem which has been used as a challenge for concurrency mechanisms since 1994. We consider this problem as an example control system, producing external signals reporting changes of internal state (that model the external world). We claim our occam-pi solution is correct-by-design but follow this up with formal verification (using the FDR model checker for CSP) that the system is free from deadlock and livelock, that the produced control signals obey crucial ordering constraints, and that the system has key liveness properties.

Item Type: Article
Uncontrolled keywords: determinacy analysis, Craig interpolants
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Programming Languages and Systems Group
Depositing User: Peter Welch
Date Deposited: 21 Sep 2012 09:49
Last Modified: 14 Apr 2014 10:29
Resource URI: http://kar.kent.ac.uk/id/eprint/30673 (The current URI for this page, for reference purposes)
  • Depositors only (login required):