UCL  IRIS
Institutional Research Information Service
UCL Logo
Please report any queries concerning the funding data grouped in the sections named "Externally Awarded" or "Internally Disbursed" (shown on the profile page) to your Research Finance Administrator. Your can find your Research Finance Administrator at http://www.ucl.ac.uk/finance/research/post_award/post_award_contacts.php by entering your department
Please report any queries concerning the student data shown on the profile page to:

Email: portico-services@ucl.ac.uk

Help Desk: http://www.ucl.ac.uk/ras/portico/helpdesk
Publication Detail
Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra
  • Publication Type:
    Conference
  • Authors:
    Brunet P, Pym D
  • Publisher:
    Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
  • Publication date:
    26/06/2020
  • Pagination:
    5:1, 5:16
  • Volume:
    167
  • Series:
    Leibniz International Proceedings in Informatics (LIPIcs)
  • Editors:
    Ariola ZM
  • Status:
    Accepted
  • Name of conference:
    5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
  • Conference place:
    Paris, France
  • Conference start date:
    29/06/2020
  • Conference finish date:
    06/07/2020
  • Keywords:
    Concurrent Kleene Algebra, Pomsets, Atomicity, Semantics, Separation, Local reasoning, Bunched logic, Frame rules
Abstract
Concurrent Kleene Algebra is an elegant tool for equational reasoning about concurrent programs. An important feature of concurrent programs that is missing from CKA is the ability to restrict legal interleavings. To remedy this we extend the standard model of CKA, namely pomsets, with a new feature, called boxes, which can specify that part of the system is protected from outside interference. We study the algebraic properties of this new model. Another drawback of CKA is that the language used for expressing properties of programs is the same as that which is used to express programs themselves. This is often too restrictive for practical purposes. We provide a logic, 'pomset logic', that is an assertion language for specifying such properties, and which is interpreted on pomsets with boxes. In contrast with other approaches, this logic is not state-based, but rather characterizes the runtime behaviour of a program. We develop the basic metatheory for the relationship between pomset logic and CKA, including frame rules to support local reasoning, and illustrate this relationship with simple examples.
Publication data is maintained in RPS. Visit https://rps.ucl.ac.uk
 More search options
UCL Researchers
Author
Dept of Computer Science
Author
Dept of Computer Science
University College London - Gower Street - London - WC1E 6BT Tel:+44 (0)20 7679 2000

© UCL 1999–2011

Search by