XC Formal Semantics

XCore Project reviews, ideas, videos and proposals.
Post Reply
User avatar
jonathan
Respected Member
Posts: 377
Joined: Thu Dec 10, 2009 6:07 pm
Contact:

XC Formal Semantics

Post by jonathan »

As XC has a solid theoretical base in CSP and avoids many of the analytically difficult features of C, it should be possible to come up with a formal semantics for the language. This will enable high-level source-to-source optimizations and transformations as well as allowing rigorous program correctness proofs.

This would be a great project with both research and practical value for anyone with an interest in programming language theory or semantics. Post here or get in touch!


Image
User avatar
jonathan
Respected Member
Posts: 377
Joined: Thu Dec 10, 2009 6:07 pm
Contact:

Post by jonathan »

So, "back in the day" Bill Roscoe did formal denotational semantics for Occam and Occam2. His list of publications is here:

http://www.comlab.ox.ac.uk/people/bill.roscoe/pubs.html

I'm guessing the papers are probably quite heavyweight but I'm not sure they are publicly available so can't check.

The semantic differences between XC and Occam are far less pronounced than the syntactic differences. Does anyone know Bill? I think he's still around. Perhaps a project for one of his PhD students... :-)
Image
jhrose
Active Member
Posts: 40
Joined: Mon Dec 14, 2009 11:18 am

Post by jhrose »

Hei,

In addition to early denotational models for CSP, Bill continues to publish trace semantics (models) for CSP and his book "Theory and Practice of Concurrency" (ISBN 0-13-674409-5) is approachable. Additionally Geoff Barrett worked on the "Semantics and Implementation of Occam", but his (unpublished?) book is rather heavyweight with proofs and took a while to "come up with".

However, aside from the academic interest in having a formal semantics for XC, to use it for something like "provably correct programs" (as part of the user-time development tools) may have several practical difficulties to overcome.

Firstly consider that the failures and divergences model (of Bill, Geoff, & co.) is computationally expensive, so only relatively small test sets are feasible in practice. Proving whole programs may take a while to run. Secondly, as a one-off, you will need to prove the XC language compilation and implementation. Recall Occam ran on the Transputer core (and was ported to other processors through front-end tools), and similarly to prove your XC code will run 'correctly' you will need to prove the language against the (XS-1) processor instruction set to which it is translated. (Of course you will also need to prove the silicon really implements the instruction set as intended too.) Maybe XMOS already have elements of these language and silicon proofs, as "XC has a solid theoretical base in CSP". Thirdly, let's assume you are able to prove your whole program runs on the hardware as planned, you need to prove it satisfies your design (and how XC programmers will input this into a tool), and relatedly, how do you know the design does what you actually intended for it (i.e. if you wrote the design right)?

Addressing issues like these would seem favourable for safety-critical systems acceptance, and maybe sponsors or awards can be found for a programme of research?
Post Reply