Transcript Presentation - The Department of Computer Science

Self-Stabilization as a
Foundation for
Autonomic Computing
Olga Brukman, Shlomi Dolev,
Yinnon A. Haviv, Reuven Yagel.
Ben-Gurion University of the Negev,
Beer-Sheva, Israel
FOFDC 2007, Vienna
Trends in Autonomic Computing




Self-healing, Self-managing, Self-*.
Recovery Oriented Computing [Berkeley,
Stanford].
Autonomic Computing [IBM].
Robust infrastructure for achieving the above is
missing.
Processor.
 Operating systems do not stabilize.
 Nothing built on top of this platform can be fully
robust.

FOFDC 2007, Vienna
Self-Stabilization: Well Established
Theory !




Self-Stabilization[Dijk’74].
Self-Stabilization [Dolev’2K].
Abstract, stand-alone
algorithms.
Self-stabilization was not
fully deployed in real-life
systems.

Self-stabilizing protocols.

FOFDC 2007, Vienna
Routing Information Protocol
(RIP).
Self-Stabilization


Self-stabilization is achieved through algorithm fully exploring the
system state space.
Self-stabilizing algorithm is continuously executed, and its code is
not corrupted.
FOFDC 2007, Vienna
Self-Stabilization as a Base for
True Autonomic Computing
 Well
defined and provable property.
 Ability to deal with unpredicted
failures.
 Automatic recovery from any state.
FOFDC 2007, Vienna
Self-Stabilization Stack
Self-Stabilizing Program
Stabilization Preserving
Compiler
Self-Stabilizing
Operating System
Self-Stabilizing Processor
FOFDC 2007, Vienna
Self-Stabilization Stack: Non SelfStabilizing Programs
Self-Stabilizing Program
Recovery Oriented
Software
Stabilization
Preserving
Compiler
Eventually Byzantine
Program
Self-Stabilizing Automatic
Recoverer
Self-Stabilizing
Operating System
Self-Stabilizing Processor
Recovery Oriented Program
FOFDC 2007, Vienna
Self-Stabilizing
Processor
Shlomi Dolev, Yinnon A. Haviv
Self Stabilizing Microprocessor

Legal execution of a processor
 Every
process starting from an arbitrary state
reaches fetch-decode-execute sequence.

What is a self-stabilizing processor?
 Every
execution of the processor starting from
an arbitrary state reaches a safe
configuration, which implies legal execution
after the safe state
FOFDC 2007, Vienna
Self-Stabilizing Processor: How?
 Verifying
self-stabilization in existing
processor
 Each
circle in the processor automata
has a fetch-decode-execute loop.
 Adding
self-stabilization to a
processor
 Using
a self-stabilizing watchdog
FOFDC 2007, Vienna
Self-Stabilizing
Operating System
Shlomi Dolev, Reuven Yagel
Self-Stabilizing Operating System

Black box
 Reloading
OS code from ROM periodically.
 The reloading function is hardwired in ROM

Tailored Solution
 Process
scheduling
 Memory management
 Device drivers
FOFDC 2007, Vienna
Tailored Solution: Scheduling
Fairness and stabilization preservation
 Periodic execution



non-maskable interrupts and watchdog
Scheduler state (process table)
correctness
 Bounded
index to fix number of processes
 Enforcing separation through segmentation
FOFDC 2007, Vienna
Tailored Solution: Memory
Management
Eventual consistency of memory hierarchy
 Stabilization preservation

 Processes
do not affect other processes
memory

Solutions
 Allocate
entire memory
 Fixed partitions with continuous monitoring
 Lease based dynamic schemes
FOFDC 2007, Vienna
Tailored Solution: Device Drivers
Device
Driver
Controller
I/O Device
OS
Self-stabilizing
protocol

Ping-pong requirement


Exchange requests and replies infinitely often
Progress requirement

Eventually every I/O request is executed according to
specifications
FOFDC 2007, Vienna
Tailored Solution: Device Drivers

Self-stabilizing protocol
1.
Lease based execution of the protocol
OR
2.
Assuming the device controller is selfstabilizing, enforces state consistency
through snapshots.
FOFDC 2007, Vienna
Tailored Solution: Implementation



Prototype based on Intel
Pentium processor
Detailed proof of the
assembly code
correctness
Our prototype shows
that it is possible to
design a self-stabilizing
OS kernel.
FOFDC 2007, Vienna
Self-Stabilization
Preserving Compiler
Shlomi Dolev, Yinnon A. Haviv,
Mooly Sagiv,
Department of Computer Science
Tel Aviv University, Israel
Non-Stabilization Preserving
Compiler
S
high abstraction
language


Compiler
T
machine
language
S and T behave the same only when started in
the initial state.
Existing compilers are non-stabilization
preserving

T may reach an unexpected state due to soft-error
experienced by microprocessor
FOFDC 2007, Vienna
Non-Stabilization Preserving
Compiler: Example
mov ax, 10
mov cx, 0
loop1:
push cx
call f
inc cx
cmp cx,ax
jne loop
for (int i=0; i<10; i++)
f(i)


Compiled code: start with cx=12 inside the loop…
Moreover: Any runtime mechanism can get stuck or
become inconsistent.

Stack, heap
FOFDC 2007, Vienna
Stabilization Preserving Compiler
Enforce invariants
Variable declarations
upon <condition_1> do
<statement_1>
S.P. Compiler
Scheduler
condition_1
…
condition_n
Statement_1
upon <condition_n> do
<statement_n>
Statement_n
FOFDC 2007, Vienna
Recovery Oriented
Software
Olga Brukman, Shlomi Dolev
Software Contains Bugs
Writing self-stabilizing software is hard
 Correct and faultless SW is hard


Long-lived running programs, e.g., OS
 Heisenbugs, corrupt states, leaked resources
are common…

Usually software is tested when starting
from initial state and considering limited
time scenarios.
FOFDC 2007, Vienna
Fault Model Reflecting Reality





Software packages can be trusted to work as
required after restart.
Eventual Byzantine software.
System administrators and users use reboot to
deal with faults.
Contract between the client, project manager and
programmers, that is checked on line!
Additional (thin) monitoring and recovering layer
is self-stabilizing.
FOFDC 2007, Vienna
Parts in Contract

Specifications Composer
(Project Manager)

Invariants and predicates


important properties on
program IO
Recovery actions
• Programmer
• Best-effort implementation
• Using same IO variables as
specifier
• Still: bugs and
unexpected states
FOFDC 2007, Vienna
26
Environment

Self-stabilizing processor + Self-stabilizing OS
Processes exist and execute their code
 Infrastructure for robust monitoring and recovery


Not immediately Byzantine
 eventual
Byzantine program
Long enough to do
sufficient job
FOFDC 2007, Vienna
Self-Stabilizing
Recoverer for Eventual
Byzantine Software
Olga Brukman, Shlomi Dolev
Hillel Kolodner,
Haifa Research Labs
IBM, Israel
Middleware Architecture
<Preds,RActs>1
<Preds,RActs>2
…
<Preds,RActs>n
OMR
Kernel
OS
FOFDC 2007, Vienna
Recovery Oriented
Programming
Olga Brukman and Shlomi Dolev
Our Framework: Transforming
Recovery Tuples into Code
External
Monitor
Subsystems
hierarchy
event-driven
monitoring
event-driven
monitoring
Recovery
tuples
External
Monitor
event-driven
monitoring
event-driven
monitoring
Pre-compiler
External
Monitor
event-driven
monitoring
Code
event-driven
monitoring
Subsystem
External
Monitor
FOFDC 2007, Vienna
31
Conclusions
Self-Stabilization as an effective paradigm
for creating robust systems.
 Rigorous approach for designing basic
system components

 Microprocessor
 Operating
system
 Compiler
 Recovery
Oriented Software
FOFDC 2007, Vienna
Faces Behind the Paper
Recovery Oriented
Software [BDK03, BD06]
Stabilization Preserving
Compiler [DHS05]
Self-Stabilizing
Operating System [DY04]
Self-Stabilizing Processor
[DH06]
FOFDC 2007, Vienna
Thank You!
Questions?