5
$\begingroup$

I'm working on a class library (C++) that can be thought of as a producer/consumer queue of producer/consumer queues. There are many queues of data, and the goal is to assign worker threads to process these queues, as needed, using coroutines. At any rate, the details aren't necessarily important to the question, but I'm struggling to wrap my head fully around the synchronization requirements.

I've started with a list of basic operations (like adding an element to the top level queue), along with some preconditions, postconditions, and what I'm calling "exclusions" which are things that are not supposed to happen during the operation. It seems to only scratch the surface though.

Finally, my question: Is there a way to model algorithms (either notation or diagram) that helps to tease out temporal ordering requirements? What needs to be locked when? What transactions need to be atomic? What order can reads/writes be carried out in?

Improve this question
$\endgroup$
1
  • $\begingroup$ Are you familiar with "happens-before" relations? $\endgroup$
    – Raphael ♦
    Feb 6, 2015 at 8:16

2 Answers 2

Reset to default
3
$\begingroup$

You have mentioned the temporal ordering of events, then you may have known about temporal logic [1] such as LTL [2] and CTL [3]. Temporal logic allows you to reason about time and thus temporal ordering of events. For instance (from [1]), one may wish to say that whenever a request is made, access to a resource is eventually granted, but it is never granted to two requestors simultaneously.

The greatest advantage of using LTL or CTL to express the properties of the system is that you can automatically verify them. This process is known as model checking [4].

There are quite a few of model checkers [5]. For instance, in SPIN, systems to be verified are described in Promela (Process Meta Language), which allows one to specify "atomic blocks" (Is this your intention of What transactions need to be atomic?)?

As for the producer/consumer problem, it has been extensively studied in the context of model checking. This lecture note uses it as an example for SPIN (you can easily find other resources). In addition, [6] verifies an edition written in SystemC, and [7] verifies it using TLA+.

[1] temporal logic (wiki)

[2] LTL (wiki)

[3] CTL (wiki)

[4] model checking (wiki)

[5] model checkers (wiki)

[6] Verifying SystemC: a Software Model Checking Approach

[7] An Example of Debugging Java with a Model Checker (web page)

Improve this answer
$\endgroup$
2
  • $\begingroup$ This is great info. Can you recommend a good entry point into studying temporal logic and other formal software engineering practices? I've been programming for 20 years, but lack a formal education. I've searched endlessly for tutorials and free materials on Google, but had little success. $\endgroup$
    – Brent
    Feb 8, 2015 at 17:31
  • 1
    $\begingroup$ @Brent For temporal logic and model checking, I would like to recommend the book "Principles of Model Checking" by Christel Baier and Joost-Pieter Katoen (MIT Press, 2008). You may also find that the book "Logic in Computer Science" by Michael Huth and Mark Ryan serves a good introduction to formal logic (including model checking). In addition, the book "Software Reliability Methods" by Doron A. Peled includes more software engineering practices. $\endgroup$
    – hengxin
    Feb 9, 2015 at 9:02
2
$\begingroup$

Usually, when trying to model concurrency, I see a lightweight version of CSP being used. It models the externally relevant behavior of a pair of processes as state machines that communicate (synchronize) by performing same-actions at the same time.

http://en.wikipedia.org/wiki/Communicating_sequential_processes

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.