Behrends

Uploaded from authorPOINT
Views:
 
     
 

Presentation Description

No description available.

Comments

Presentation Transcript

The Universe Model: An Approach for Improving the Modularity and Reliability of Concurrent Programs: 

The Universe Model: An Approach for Improving the Modularity and Reliability of Concurrent Programs Reimer Behrends and Kurt Stirewalt Dept. of Comp. Science and Eng. Michigan State University

Overview: 

Overview Motivation and Goals Description of the Universe Model Benefits of the Universe Model Related Work and Conclusions

Design vs. Concurrency: 

Design vs. Concurrency Course 0+ Has-prereq (Course) CSE914 (Course) CSE470 (Course) MTH472 Has-prereq Has-prereq

Capturing the Design: 

Capturing the Design Enrollment: synchronized cse914, cse470, mth472 do if cse914.has_room and cse914.satisfies_prereq(student) then cse914.enroll(student) end end

Goals: 

Goals Implementation should mirror the design. Separation and abstraction of concurrency concerns. Composability of concurrent components. Reliability on par with sequential programs.

Overview: 

Overview Motivation and Goals Description of the Universe Model Benefits of the Universe Model Related Work and Conclusions

The Universe Model: 

The Universe Model Universes are sets of objects. Public objects + auxiliary objects. Simple routines execute within universes. Realms are sets of universes. Dynamic and recursive assembly of universes. Based on concurrency constraints. Processes execute within realms. Realms don’t intersect.

Concurrency Constraints: 

Concurrency Constraints Example: Dining Philosophers Philosophers, forks are universes. Concurrency constraint: eating =andgt; left_fork and right_fork Condition Variable Universe Variables

Code and Concurrency Constraints: 

Code and Concurrency Constraints Code attribute eating: BOOLEAN; loop think; eating := true; eat(left_fork, right_fork); eating := false; end Constraint concurrency eating =andgt; left_fork and right_fork

Scheduling = Satisfiability: 

Scheduling = Satisfiability Concurrency constraints are correctness conditions. Constraint satisfiable =andgt; Process can be scheduled. Constraint not satisfiable =andgt; Process blocks.

Dining Philosophers: 

Dining Philosophers Philosophers, forks are universes. Concurrency constraint: eating =andgt; left_fork and right_fork P1 P5 P2 P4 P3 F F F F F

Dining Philosophers: 

Dining Philosophers Philosophers, forks are universes. Concurrency constraint: eating =andgt; left_fork and right_fork P1 P5 P2 P4 P3 F F F F F

Overview: 

Overview Motivation and Goals Description of the Universe Model Benefits of the Universe Model Related Work and Conclusions

Benefits of the Universe Model: 

Benefits of the Universe Model Abstraction Separability Reification of Design Composability Redundancy Security

Code, Constraints, Abstract State: 

Code, Constraints, Abstract State Code loop think; eating := true; eat(left_fork, right_fork); eating := false; end Constraint eating =andgt; left_fork and right_fork Abstract State eating: BOOLEAN;

Composability: 

Composability Dependency hidden from clients of CSE470. Global realm computation based on local concurrency constraints. (Course) CSE914 (Course) CSE470 (Course) MTH472 Has-prereq Has-prereq concurrency CSE470 and MTH472

Reliability: 

Reliability Common programming constructs have safety mechanisms. Arrays: Range check for indices. Pointers: Garbage collection avoids dangling points and memory leaks. Generally no such mechanism for mutual exclusion.

Security through Redundancy: 

Security through Redundancy Runtime error when: Incorrect implementation =andgt; violates correct concurrency constraint =andgt; runtime error. Incorrect concurrency constraint =andgt; correct implementation breaks =andgt; runtime error.

Overview: 

Overview Problems and Goals Description of the Universe Model Benefits of the Universe Model Related Work and Conclusions

Related Work: 

Related Work Coordination languages like Linda, Strand, Manifold, etc. also attempt to separate coordination from computation. Computational and coordination parts often still interleaved. Don’t implicitly provide a safety mechanism. Often rely on referential transparency.

Conclusions: 

Conclusions Universe model allows to map the design onto the implementation in a straightforward fashion. Concurrency concerns are factored out. Components become easily composable. Redundancy increases security.

Efficiency: 

Efficiency SAT is NP-hard. Don’t need negation of universe variables—there is usually no point in requiring that we not access a universe. Represent reduced formula in DNF. Satisfy by picking a clause at random. Bitmapped representation for further efficiency.

Starvation: 

Starvation Scheduling in the universe model non-trivial. Deal with multiple locks without risk of starvation. Existing algorithm: pSather scheduler. Our approach: Quantum queues (probabilistic scheduling).

Example II: Producer/Consumer: 

Example II: Producer/Consumer Consumer: reading =andgt; not queue.is_empty and queue Producer: writing =andgt; not queue.is_full and queue Producer Queue Consumer

Example II: Producer/Consumer: 

Example II: Producer/Consumer Consumer: reading =andgt; not queue.is_empty and queue Producer: writing =andgt; not queue.is_full and queue Producer Queue Consumer Data

Example II: Producer/Consumer: 

Example II: Producer/Consumer Consumer: reading =andgt; not queue.is_empty and queue Producer: writing =andgt; not queue.is_full and queue Producer Queue Consumer Data