|
|
|
|
| LEADER |
05914nam a2200325Ia 4500 |
| 001 |
2526 |
| 003 |
WAA |
| 005 |
20240514062538.0 |
| 006 |
a||||fr|||| 001 0 |
| 007 |
ta |
| 008 |
t xxk-|||||r|||| 001 0 rpa d |
| 999 |
|
|
|c 2526
|d 2526
|
| 020 |
|
|
|a 9780321312839
|
| 040 |
|
|
|c WAA
|a WAA
|
| 041 |
|
|
|a eng
|
| 100 |
1 |
|
|a Ben-Ari, Mordechai
|9 2788
|
| 245 |
1 |
0 |
|a Principles of concurrent and distributed programming /
|c Mordechai Ben-Ari
|
| 250 |
|
|
|a 2nd. ed.
|
| 260 |
|
|
|a Harlow :
|b Addison-Wesley,
|c 2006
|
| 300 |
|
|
|a 361 p.
|
| 505 |
|
|
|a Preface -- 1 What is Concurrent Programming? -- 1.1 Introduction -- 1.2 Concurrency as abstract parallelism -- 1.3 Multitasking -- 1.4 The terminology of concurrency -- 1.5 Multiple computers -- 1.6 The challenge of concurrent programming -- 2 The Concurrent Programming Abstraction -- 2.1 The role of abstraction -- 2.2 Concurrent execution as interleaving of atomic statements -- 2.3 Justification of the abstraction -- 2.4 Arbitrary interleaving -- 2.5 Atomic statements -- 2.6 Correctness -- 2.7 Fairness -- 2.8 Machine-code instructions -- 2.9 Volatile and non-atomic variables -- 2.10 The BACI concurrency simulator -- 2.11 Concurrency in Ada -- 2.12 Concurrency in Java -- 2.13 Writing concurrent programs in Promela -- 2.14 Supplement: the state diagram for the frog puzzle -- 3 The Critical Section Problem -- 3.1 Introduction -- 3.2 The definition of the problem -- 3.3 First attempt -- 3.4 Proving correctness with state diagrams -- 3.5 Correctness of the first attempt -- 3.6 Second attempt -- 3.7 Third attempt -- 3.8 Fourth attempt -- 3.9 Dekker’s algorithm -- 3.10 Complex atomic statements -- 4 Verification of Concurrent Programs -- 4.1 Logical specification of correctness properties -- 4.2 Inductive proofs of invariants -- 4.3 Basic concepts of temporal logic -- 4.4 Advanced concepts of temporal logic -- 4.5 A deductive proof of Dekker’s algorithm -- 4.6 Model checking -- 4.7 Spin and the Promela modeling language -- 4.8 Correctness specifications in Spin -- 4.9 Choosing a verification technique -- 5 Advanced Algorithms for the Critical Section Problem -- 5.1 The bakery algorithm -- 5.2 The bakery algorithm for N processes -- 5.3 Less restrictive models of concurrency -- 5.4 Fast algorithms -- 5.5 Implementations in Promela -- 6 Semaphores -- 6.1 Process states -- 6.2 Definition of the semaphore type -- 6.3 The critical section problem for two processes -- 6.4 Semaphore invariants -- 6.5 The critical section problem for N processes -- 6.6 Order of execution problems -- 6.7 The producer–consumer problem -- 6.8 Definitions of semaphores -- 6.9 The problem of the dining philosophers -- 6.10 Barz’s simulation of general semaphores -- 6.11 Udding’s starvation-free algorithm -- 6.12 Semaphores in BACI -- 6.13 Semaphores in Ada -- 6.14 Semaphores in Java -- 6.15 Semaphores in Promela -- 7 Monitors -- 7.1 Introduction -- 7.2 Declaring and using monitors -- 7.3 Condition variables -- 7.4 The producer–consumer problem -- 7.5 The immediate resumption requirement -- 7.6 The problem of the readers and writers -- 7.7 Correctness of the readers and writers algorithm -- 7.8 A monitor solution for the dining philosophers -- 7.9 Monitors in BACI -- 7.10 Protected objects -- 7.11 Monitors in Java -- 7.12 Simulating monitors in Promela -- 8 Channels -- 8.1 Models for communications -- 8.2 Channels -- 8.3 Parallel matrix multiplication -- 8.4 The dining philosophers with channels -- 8.5 Channels in Promela -- 8.6 Rendezvous -- 8.7 Remote procedure calls -- 9 Spaces -- 9.1 The Linda model -- 9.2 Expressiveness of the Linda model -- 9.3 Formal parameters -- 9.4 The master–worker paradigm -- 9.5 Implementations of spaces -- 10 Distributed Algorithms -- 10.1 The distributed systems model -- 10.2 Implementations -- 10.3 Distributed mutual exclusion -- 10.4 Correctness of the Ricart–Agrawala algorithm -- 10.5 The RA algorithm in Promela -- 10.6 Token-passing algorithms -- 10.7 Tokens in virtual trees -- 11 Global Properties -- 11.1 Distributed termination -- 11.2 The Dijkstra–Scholten algorithm -- 11.3 Credit-recovery algorithms -- 11.4 Snapshots -- 12 Consensus -- 12.1 Introduction -- 12.2 The problem statement -- 12.3 A one-round algorithm -- 12.4 The Byzantine Generals algorithm -- 12.5 Crash failures -- 12.6 Knowledge trees -- 12.7 Byzantine failures with three generals -- 12.8 Byzantine failures with four generals -- 12.9 The flooding algorithm -- 12.10 The King algorithm -- 12.11 Impossibility with three generals -- 13 Real-Time Systems -- 13.1 Introduction -- 13.2 Definitions -- 13.3 Reliability and repeatability -- 13.4 Synchronous systems -- 13.5 Asynchronous systems -- 13.6 Interrupt-driven systems -- 13.7 Priority inversion and priority inheritance -- 13.8 The Mars Pathfinder in Spin -- 13.9 Simpson’s four-slot algorithm -- 13.10 The Ravenscar profile -- 13.11 UPPAAL -- 13.12 Scheduling algorithms for real-time systems -- A The Pseudocode Notation -- B Review of Mathematical Logic -- B.1 The propositional calculus -- B.2 Induction -- B.3 Proof methods -- B.4 Correctness of sequential programs -- C Concurrent Programming Problems -- D Software Tools -- D.1 BACI and jBACI -- D.2 Spin and jSpin -- D.3 DAJ -- E Further Reading.
|
| 650 |
|
4 |
|6 Informática
|9 13
|
| 650 |
|
4 |
|a Programación informática
|9 14
|
| 650 |
|
4 |
|a Diseño de sistemas
|9 705
|
| 650 |
|
4 |
|9 5651
|a Programación concurrente
|
| 650 |
|
4 |
|9 5650
|a Programación distribuida
|
| 942 |
|
|
|2 CDU
|c LIBRO
|
| 952 |
|
|
|0 0
|1 0
|2 CDU
|4 0
|6 004_420000000000000_B4301
|7 0
|9 371
|a 09
|b 09
|d 2017-10-18
|l 0
|o 004.42 B4301
|p 10-04478
|r 2017-10-18
|w 2017-10-18
|y LIBRO NPP
|
| 952 |
|
|
|0 0
|1 0
|2 CDU
|4 0
|6 004_420000000000000_B4301
|7 0
|9 372
|a 09
|b 09
|d 2017-10-18
|l 0
|o 004.42 B4301
|p 10-04479
|r 2017-10-18
|w 2017-10-18
|y LIBRO
|
| 952 |
|
|
|0 0
|1 0
|2 CDU
|4 0
|6 004_420000000000000_B4301
|7 0
|9 10632
|a 09
|b 09
|d 2018-03-23
|l 0
|o 004.42 B4301
|p 10-06172
|r 2018-03-23
|w 2018-03-23
|y LIBRO
|