| << Chapter < Page | Chapter >> Page > |
Concurrency is the execution of two or more independent, interacting programsover the same period of time; their execution can be interleaved or even simultaneous.Concurrency is used in many kinds of systems, both small and large.
The typical home computer is full of examples. In separate windows, a user runs a web browser, a text editor, and a music playerall at once. The operating system interacts with each of them.
Almost unnoticed, the clock and virus scanner are also running. The operating system waits for the user to ask more programs tostart, while also handling underlying tasks such as resolving what information from the Internet goes to which program.
Using a web-based airline reservation system, Joe and Sue each want to buy a ticket.Each has a separate computer, and thus a separate web browser. Their two web browsers plus the airline's web server togethercomprise the concurrent program.
As this example illustrates, the term concurrent system might be more appropriate. However, for verification purposes, we willview them as a single, distributed entity to be modeled.
A concurrent system may be implemented via process es and/or thread s. Although details can vary upon platform, the fundamentaldifference is that processes have separate address spaces, whereas threads share address spaces.We will follow the common theoretical practice and ignore this distinction, using shared variables when desired, and using the twoterms interchangeably.
We view these threads as executing relatively independently. However, since they are acting together towards some goal,they must need to communicate and coordinate. The two most common communication techniques in processes and threadsare through, respectively, message passing and shared variables . In order to communicate at the right times,they must synchronize , together arriving at agreed-upon control points. Often, one or morethreads block , or stop and wait for some external event. In this module, we will use only shared variables,although the tools we use also allow message passing.
Even though we have multiple flows of control, that doesn't imply we need multiple processors. Concurrent programs may beexecuted on a single processor by interleaving their control flows. In order to understand what happens in a concurrent program over time,we must understand how the individual operations of the threads can interleave. This is independent of how many processesorswe use, although it is convenient to think of only having one processor.To consider the possible interleavings, we need to know which actions are atomic , or indivisible. If an atomic operation begins,we know that it won't be interrupted by a context switch until it is done.We generally assume that each hardware machine instruction is atomic, but a programming language might guarantee that even more complicatedoperations are atomic as well.
Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|