[concurrency-interest] Ensuring the correctness of concurrent code

Szabolcs Ferenczi szabolcs.ferenczi at gmail.com
Wed Sep 3 19:16:41 EDT 2014


Hi, I have used CSP before and I liked it. It is very powerful but it needs
a special thinking when you try to map the procedural language notation
such as Java into the CSP notation. It is better to generate the mapping if
possible. Even better to model first and generate the code from the model.
In the book Concurrency: State Models & Java Programs the authors show a
way how to do the mapping by hand. You need to deal with the memory model
at the lowest level though. The advantage of the CSP notation is that you
can model your program at different abstraction levels and check that the
refinement still holds between the levels.
--
Szabolcs


On 3 September 2014 22:49, Chris Vest <mr.chrisvest at gmail.com> wrote:

> Hi,
>
> I occasionally have to write code that does shared mutable memory
> concurrency, have high performance requirements, and needs a high degree of
> confidence in the correctness of the implementation.
>
> So far I have tackled this by thinking hard and working hard. I’ve written
> hundreds of tests for tiny APIs, targeted and randomised alike, I’ve drawn
> up diagrams summarising all the state transitions, I’ve gone through the
> code to check every against said diagram, I’ve written documentation to
> specify all observable behaviours, and then written more tests for things I
> discovered while writing said documentation, sleep on it, wake up and write
> even more tests for new scenarios I’ve literally dreamt up. And so on…
>
> This has worked well so far, though it takes a lot of effort and
> discipline. However, as the problems I try to solve get harder, and the
> optimisations I want to pull off gets more cunning, I feel like I’m
> approaching the limits of this “technique.”
>
> So, how to other people approach this? How is the correctness of the
> j.u.c. implementations ensured, for instance?
>
> I have begun studying TLA+ in the hope that the formal specifications
> might be helpful, but I’m not sure if that’s the right path. I haven’t
> studied proof techniques before. One worry I have with TLA+ is how to
> accurately represent the given memory model I’m working with, which has
> thus far been the JMM.
>
> Cheers,
> Chris
>
>
> _______________________________________________
> Concurrency-interest mailing list
> Concurrency-interest at cs.oswego.edu
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://cs.oswego.edu/pipermail/concurrency-interest/attachments/20140904/26a50a65/attachment.html>


More information about the Concurrency-interest mailing list