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 highlevel sourcetosource 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!
XC Formal Semantics

 Respected Member
 Posts: 377
 Joined: Thu Dec 10, 2009 6:07 pm

 Respected Member
 Posts: 377
 Joined: Thu Dec 10, 2009 6:07 pm
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... :)
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... :)

 Active Member
 Posts: 40
 Joined: Mon Dec 14, 2009 11:18 am
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 0136744095) 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 usertime 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 oneoff, 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 frontend tools), and similarly to prove your XC code will run 'correctly' you will need to prove the language against the (XS1) 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 safetycritical systems acceptance, and maybe sponsors or awards can be found for a programme of research?
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 0136744095) 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 usertime 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 oneoff, 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 frontend tools), and similarly to prove your XC code will run 'correctly' you will need to prove the language against the (XS1) 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 safetycritical systems acceptance, and maybe sponsors or awards can be found for a programme of research?