| << Chapter < Page | Chapter >> Page > |
Both the syntax and semantics of the concurrency primitives can vary among programming languages and concurrency libraries.We will use a particular language, Promela , which implements the most commonly-used features ofconcurrent programs. In Promela,assignment statements are defined to be atomic. We'll later contrast atomic with non-atomic assignment statements.
Programmers are comfortable with debugging single-threaded code, where most questions involve ``doesthis sequence of instructions compute the correct answer?''Concurrency, however, introduces the added complications of communication and synchronization;a single task may be spread across several sequences of instructions running asynchronously,and multiple threads can interact in unintended ways. The following are five common categories of problems with concurrency.
As an analogy, consider two people walking in a hallway towards each other. The hallway is wide enough for twopeople to pass. Of interest is what happens when the two people meet.If on the same side of the hallway, a polite strategy is to step to the other side.A more belligerent strategy is to wait for the other person to move. Two belligerent people will suffer in deadlock, glaringface to face in front of each other. Two polite people could suffer from livelockif they repeatedly side-step simultaneously. (No conclusions on morality are to be inferred fromthe fact that one polite and one belligerent person don't have any problems.)
There are more specific notions of fairness that describe when and how often threads are guaranteed to get a turn.For example, do we expect that each thread should be executed as often as any other, or is it acceptable if one runs a hundred stepsfor each step of any other thread? When considering fairness, one must also consider the system codeimplementing the threads. The implementation includes a scheduler that determines how to interleave the threads, and the schedulermight or might not provide any fairness guarantees.
Assume we are modeling a store. Consumers buy products, reducing the shelf inventory. Meanwhile, employees restockthe shelves, increasing the shelf inventory. More simply, let thread be a loop that repeatedly decrements a counter, and thread be a loop that repeatedly increments that same counter.
Unless our scheduler (which may be nature) otherwise gives some guarantees,this system does not ensure that the two threads execute fairly.In particular, it is possible for one thread to starve the other.
Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|