How to make our system reliable?
Menu Menu
Requirements
We need reliable society
Quick development of complex system
Such as
Web service
Car system
Economic System (Bank / Stock Market )
Government System (Tax / Services )
Security
Keeping secrets are very small part of security.
System must keep working
high availability
correctly working
System may fail (ex. hardware failure, fire)
Backup is important
Accessibility
Unusable system is the most safe one?
compromise ( such as 4 digit password)
Human factor
Technology itself does not make the system reliable
be a reliable person
Difficulty
System is large and complex
Hardware
Finite automaton ( looping on fix amount of state, very simple)
CPU
Memory
Network
It is very fast and very large now.
Software
Operating system
Application
Services
Framework
Library
Database
Concurrency
Distributed System
Parallel System
Concurrency in Java
Permutation of events
Java Thread Interleave Example
% java interleave.Interleave
Thread t1 created.
Thread t2 created.
Thread t3 created.
t2 t2 t3 t3
何回か動かすと、
t2 t3 t2 t3
とかが見れるはずだが...
Specification / Implementation / Execution
Specification in logic
Implement in functions
Execution result is set
First order logic
p p is true
¬ p p is not true
p ∧ q p and q is true
p ∨ q p or q is true
p → q p implies q ( ¬ p ∨ q )
formula and it's meanings.
value of variables
assert
all assertions are correct (valid)
in any permutated executions
Temporal Logic
□p always p
◇p sometimes p
◇p = ¬ □ ¬ p
Tools to check reliability
Proof implementation → specification
Check assertion
Proof system
Proofs in a first order logic is an function ( lambda calculus)
Write down the proofs as a function
Coq
Agda
Model checking system
Execute all possible permutation and check assertion
SPIN
SMV
Java PathFinder
Java Pathfinder
前のinterleaveの例題を Java Pathfinderで実行してみる。すべての組み合わせが生成されていることを確かめよう。
% ant build
Buildfile: /Users/kono/Sites/lecture/os/ex/problem/interleave/build.xml
build:
[javac] /Users/kono/Sites/lecture/os/ex/problem/interleave/build.xml:9: warning: 'includeantruntime' was not set, defaulting to build.sysclasspath=last; set to false for repeatable builds
BUILD SUCCESSFUL
Total time: 0 seconds
+leo+kono jpf +classpath=. threadTest.TestThread
[SEVERE] cannot load application class threadTest.TestThread
% ls
build.xml index.html interleave/ interleave.tgz
% jpf +classpath=. interleave.Interleave
JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.
====================================================== system under test
interleave.Interleave.main()
====================================================== search started: 12/28/15 9:59 PM
Thread t1 created.
Thread t2 created.
Thread t3 created.
t2 t2 t3 t3
t2 t2 t3 t3
t2 t3 t2 t3
t2 t3 t2 t3
t2 t3 t3 t2
t2 t3 t3 t2
t3 t2 t2 t3
t3 t2 t2 t3
t3 t2 t3 t2
t3 t2 t3 t2
t3 t3 t2 t2
t3 t3 t2 t2
t2 t2 t3 t3
t2 t3 t2 t3
t2 t3 t3 t2
t3 t2 t2 t3
t3 t2 t3 t2
t3 t3 t2 t2
====================================================== results
no errors detected
====================================================== statistics
elapsed time: 00:00:00
states: new=1999,visited=2614,backtracked=4613,end=18
search: maxDepth=48,constraints=0
choice generators: thread=1999 (signal=0,lock=174,sharedRef=1576,threadApi=66,reschedule=183), data=0
heap: new=1921,released=1886,maxLive=385,gcCycles=4313
instructions: 33087
max memory: 245MB
loaded code: classes=63,methods=1476
====================================================== search finished: 12/28/15 9:59 PM
Difficulty
proof system is *very* difficult
Model checking requires large amount of computation
Continuous Integration
A practical solution in Web service system
Automatic deployment with automatic test
Jenkins
Exercise 1.1
Write down all possible permutation for three threads in interleave.Interleave
Send report to
kono@ie.u-ryukyu.ac.jp
as a
Subject: Frontier of Engineering Exercise 1.1
2016/1/12