Idempotence Bugs in Intermittent Systems

I/O Dependent Idempotence Bugs
in Intermittent Systems
Milijana Surbatovich
,
Limin Jia, and Brandon Lucia
1
 
Energy-harvesting devices (EHDs) enable computing in
inaccessible environments
Batteries:
expensive or impossible to access and replace
maintenance can be intrusive
 
2
Intermittence in energy harvesting devices
Energy Buffer
Harvester
3
Powers on as
energy is available
Hardware platform
Intermittence in energy harvesting devices
4
Powers off at arbitrary
program location
Volatile state clears,
persistent state remains
Energy Buffer
Harvester
Hardware platform
B
 
x := y
 
y := 5
Background: intermittent execution causes bugs
B
 
Power fail
5
A
B
C
A
B
Re-execution must
be idempotent
B
 
x := y
 
y := 5
Write-after-read:
no dataflow
Re-execution
causes dataflow
Current systems provide forward progress and
fix WAR bugs – is this enough?
Need to back up
original value
Save volatile
state periodically
What about input operations?
6
B
 
x := input()
 
y := x
B
 
x := input()
 
y := x
A different value
on re-execution?
Current systems miss bugs caused by input
Repeating input operations causes unaddressed bugs
Want to port existing code-bases
Prior systems only address progress and WAR bugs
7
Outline
How intermittence causes bugs without system support
Repeated I/O operations can cause idempotence bugs
IBIS, a tool for detecting bugs caused by I/O operations
Evaluation and conclusion
8
Repeated I/O reads cause idempotence bugs
get_temp() -> cold
input < limit
steady := 1
 
Execution Time
Control dependence
on I/O causes
inconsistent updates!
 
steady
0
 
blink
0
 
steady
1
 
blink
0
1
1
9
input := get_temp()
if (input < limit):
    steady := 1
else:
    blink := 1
assert(blink^steady)
get_temp() -> hot
input > limit
blink := 1
assert == false
Simple fix can break program timeliness
 
10
J. Hester, K. Storer, and J. Sorber. Timely Execution on
Intermittently Powered Batteryless Sensors. (SenSys '17)
get_temp() -> cold
input < limit
steady := 1
 
Execution Time
if (input < limit):
    steady := 1
else:
    blink := 1
assert(blink^steady)
input := get_temp()
(input == cold)
input < limit
steady := 1
Detecting I/O bugs is particularly important for EHDs
11
get_temp() -> cold
get_temp() -> hot
 
get_temp() -> cold
We characterize input-dependent bugs for the first time
 
Sensor driven
 
Input causes bugs
 
No simple fix
Outline
How intermittence causes bugs without system support
Repeated I/O operations can cause idempotence bugs
IBIS, a tool for detecting bugs caused by I/O operations
IBIS-Static – less precise, full coverage, no runtime cost
IBIS-Dynamic – no false positives, may have less coverage, runtime cost
Evaluation and conclusion
12
Uses standard taint analysis
Reports bug patterns to the programmer
IBIS-S: static taint analysis and pattern matching
Taint Analysis
13
Bug Pattern
Matching
Report
Taint analysis: tracks dataflow off inputs
LLVM analysis pass, programmer annotates tainted source
14
input := 
get_temp()
if (input < limit):
    steady := 1
else:
    blink := 1
alert(blink)
 
Algorithm
 
1.
Mark uses of annotated
functions as 
tainted
,
add to worklist
 
2.
Get item from list,
propagate taint to any
uses
 
3.
If a branch is tainted,
propagate taint to any
dependent stores
Repeat until
list is empty
Taint analysis: interprocedural flows
15
func sample:
  io_src = getTemp()
  process(io_src)
func process(temp):
  sink = temp
 
Function arguments
input := 
get_temp()
if (input < limit):
    steady := 1
else:
    blink := 1
alert(blink)
alert(val):
    if (val):
       events++
Also: global variables,
return statements,
pass-by-ref parameters
Bug pattern matching
 
Bug Pattern
if input < limit
blink = 1
 
blink
 
s0:
steady = 1
 
s1:
A tainted branch with paths that write to 
different
 variables
if input < limit
blink = 1
steady  =0
 
s0:
blink = 0
steady = 1
 
s1:
 
blink
steady
 
blink
steady
 
blink
steady
16
 
Safe Pattern
Pass outputs bug report of the tainted branch and
differing variables to the programmer
Outline
How intermittence causes bugs without system support
Repeated I/O operations can cause idempotence bugs
IBIS, a tool for detecting bugs caused by I/O operations
IBIS-Static – less precise, full coverage, no runtime cost
IBIS-Dynamic – no false positives, may have less coverage, runtime cost
Evaluation and conclusion
17
IBIS-D: dynamic taint and freshness propagation
18
 
z := y
 
w := x
 
y := input
 
fresh
 
taint
An execution must not
read a stale, tainted value
Taint: input
dependent?
Fresh: written on the
current execution?
1
 
x
 
y
 
z
 
w
0
0
0
0
0
 
1.
Shadow memory to
record metadata
 
2.
Compiler pass to instrument
calls to runtime library
0
0
1
1
1
1
Runtime warning
 
Implementation
Outline
How intermittence causes bugs without system support
Repeated I/O operations can cause idempotence bugs
IBIS, a tool for detecting bugs caused by I/O operations
IBIS-Static – less precise, full coverage, low overhead
IBIS-Dynamic – no false positives, may have less coverage, runtime cost
Evaluation and conclusion
19
Goal of evaluation
Does IBIS-S provide usable reports to the programmer?
Does IBIS-D have reasonable overheads?
20
Reported
Bugs
False
Positives
IBIS-D
 
Evaluation methodology for IBIS-S
21
Embedded
system drivers
Existing
intermittent apps
IBIS-S
Manual
categorization
Software
validation
IBIS-S finds bugs with few false positives
22
Sensor drivers more
likely to have bugs
Not I/O driven – no bugs
Blank bar means no
reports generated
Evaluation methodology for IBIS-D
23
Existing
intermittent apps
IBIS-D
Embedded
system drivers
Compare
runtimes
Extract
Bugs
IBIS-D
Compare
runtimes
IBIS-D performance
24
Constant shadow
memory overhead
Normalized to continuous unaltered
25x mean slowdown
against unaltered
(in-line with valgrind)
Comparison and limitations of IBIS-S and IBIS-D
25
Sound
(Reported bugs are true bugs)
Complete
(Finds all bugs)
IBIS-S
IBIS-D
??
Opaque path conditions,
may-write set
Alias imprecision
Exploring all paths?
Interesting challenges uncovered
26
 
Symbolic execution?
 
Safe instrumentation
 
Path
 
Power failure
 
Restart point
 
Path’
Read more in the paper
Discussion of how IBIS-S integrates with differing execution
models
Implementation details
More evaluation for both systems
Case studies of a selection of bugs
27
Summary and take-aways
We characterize I/O idempotence bugs, not addressed by prior systems, and find
they exist in real code
IBIS-S provides information to programmers about hard-to-reason about I/O
dependences
IBIS-D detects concrete bug instances when running on real energy-harvesting
hardware
28
 
I/O Dependent Idempotence Bugs in
Intermittent Systems
Milijana Surbatovich, Limin Jia, Brandon Lucia
Slide Note
Embed
Share

Energy-harvesting devices enable computing in inaccessible environments, but intermittent execution can lead to bugs and inconsistent updates. The impact of I/O-dependent idempotence bugs in intermittent systems is explored, highlighting the challenges and the need for tools like IBIS for bug detection. Repeated I/O operations can cause issues, especially with input operations, making bug detection and resolution crucial in these environments.

  • Idempotence Bugs
  • Intermittent Systems
  • Energy Harvesting Devices
  • I/O Operations
  • Bug Detection

Uploaded on Oct 04, 2024 | 0 Views


Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.

E N D

Presentation Transcript


  1. I/O Dependent Idempotence Bugs in Intermittent Systems Milijana Surbatovich, Limin Jia, and Brandon Lucia 1

  2. Energy-harvesting devices (EHDs) enable computing in inaccessible environments Batteries: expensive or impossible to access and replace maintenance can be intrusive 2

  3. Intermittence in energy harvesting devices Harvester Hardware platform Energy Buffer Powers on as energy is available 3

  4. Intermittence in energy harvesting devices Volatile state clears, persistent state remains Harvester Hardware platform Powers off at arbitrary program location Energy Buffer 4

  5. Background: intermittent execution causes bugs B x := y Save volatile state periodically A Write-after-read: no dataflow A Re-execution causes dataflow y := 5 B B B x := y Need to back up original value Power fail Re-execution must be idempotent y := 5 C B Current systems provide forward progress and fix WAR bugs is this enough? 5

  6. What about input operations? B x := input() y := x B A different value on re-execution? x := input() y := x 6

  7. Current systems miss bugs caused by input Repeating input operations causes unaddressed bugs Want to port existing code-bases Prior systems only address progress and WAR bugs 7

  8. Outline How intermittence causes bugs without system support Repeated I/O operations can cause idempotence bugs IBIS, a tool for detecting bugs caused by I/O operations Evaluation and conclusion 8

  9. Repeated I/O reads cause idempotence bugs Control dependence on I/O causes inconsistent updates! input := get_temp() get_temp() -> cold input < limit steady := 1 1 steady 0 blink if (input < limit): steady := 1 else: blink := 1 0 Execution Time get_temp() -> hot input > limit blink := 1 assert == false steady 1 blink 0 1 assert(blink^steady) 9

  10. Simple fix can break program timeliness get_temp() -> cold input < limit steady := 1 input := get_temp() Execution Time if (input < limit): steady := 1 else: blink := 1 (input == cold) input < limit steady := 1 assert(blink^steady) J. Hester, K. Storer, and J. Sorber. Timely Execution on Intermittently Powered Batteryless Sensors. (SenSys '17) 10

  11. Detecting I/O bugs is particularly important for EHDs Sensor driven No simple fix Input causes bugs get_temp() -> cold get_temp() -> cold get_temp() -> hot We characterize input-dependent bugs for the first time 11

  12. Outline How intermittence causes bugs without system support Repeated I/O operations can cause idempotence bugs IBIS, a tool for detecting bugs caused by I/O operations IBIS-Static less precise, full coverage, no runtime cost IBIS-Dynamic no false positives, may have less coverage, runtime cost Evaluation and conclusion 12

  13. IBIS-S: static taint analysis and pattern matching Uses standard taint analysis Reports bug patterns to the programmer Bug Pattern Matching Taint Analysis Report 13

  14. Taint analysis: tracks dataflow off inputs LLVM analysis pass, programmer annotates tainted source Algorithm input := get_temp() 1. Mark uses of annotated functions as tainted, add to worklist if (input < limit): Repeat until list is empty steady := 1 2. Get item from list, propagate taint to any uses else: blink := 1 3. If a branch is tainted, propagate taint to any dependent stores alert(blink) 14

  15. Taint analysis: interprocedural flows input := get_temp() if (input < limit): Function arguments steady := 1 func sample: io_src = getTemp() process(io_src) else: blink := 1 func process(temp): sink = temp alert(blink) alert(val): Also: global variables, return statements, pass-by-ref parameters if (val): events++ 15

  16. Bug pattern matching A tainted branch with paths that write to different variables Bug Pattern Safe Pattern if input < limit if input < limit s0: s0: s1: s1: blink = 1 steady =0 blink steady blink = 0 steady = 1 blink steady blink = 1 steady = 1 blink steady blink Pass outputs bug report of the tainted branch and differing variables to the programmer 16

  17. Outline How intermittence causes bugs without system support Repeated I/O operations can cause idempotence bugs IBIS, a tool for detecting bugs caused by I/O operations IBIS-Static less precise, full coverage, no runtime cost IBIS-Dynamic no false positives, may have less coverage, runtime cost Evaluation and conclusion 17

  18. IBIS-D: dynamic taint and freshness propagation Taint: input dependent? Fresh: written on the current execution? Implementation An execution must not read a stale, tainted value 1. Shadow memory to record metadata taint fresh x 0 1 2. Compiler pass to instrument calls to runtime library y := input y 0 1 0 1 z := y w := x z 0 1 0 1 w 0 0 Runtime warning 18

  19. Outline How intermittence causes bugs without system support Repeated I/O operations can cause idempotence bugs IBIS, a tool for detecting bugs caused by I/O operations IBIS-Static less precise, full coverage, low overhead IBIS-Dynamic no false positives, may have less coverage, runtime cost Evaluation and conclusion 19

  20. Goal of evaluation Does IBIS-S provide usable reports to the programmer? Reported Bugs False Positives Does IBIS-D have reasonable overheads? IBIS-D 20

  21. Evaluation methodology for IBIS-S Embedded system drivers Manual categorization Software validation IBIS-S Existing intermittent apps 21

  22. IBIS-S finds bugs with few false positives Bug report breakdown 6 Blank bar means no reports generated 5 4 3 2 1 0 mpu hdc bmp opt tmp wsn elink rfid prox gest hmc temp ar bc bfish cem ckoo rsa NoBug NoUse TrueBug Not I/O driven no bugs Sensor drivers more likely to have bugs 22

  23. Evaluation methodology for IBIS-D Extract Bugs IBIS-D Embedded system drivers Compare runtimes IBIS-D Existing Compare runtimes intermittent apps 23

  24. IBIS-D performance Constant shadow memory overhead Normalized runtimes, continuous power 70 60 25x mean slowdown against unaltered (in-line with valgrind) 50 Slowdown 40 30 20 10 0 mpux hdcx bmpx optx tempx wsnx elinkx ar bc cem cuckoo Normalized to continuous unaltered 24

  25. Comparison and limitations of IBIS-S and IBIS-D IBIS-D IBIS-S Opaque path conditions, may-write set Sound (Reported bugs are true bugs) Complete (Finds all bugs) ?? Exploring all paths? Alias imprecision 25

  26. Interesting challenges uncovered Symbolic execution? Safe instrumentation Restart point Path Path Power failure 26

  27. Read more in the paper Discussion of how IBIS-S integrates with differing execution models Implementation details More evaluation for both systems Case studies of a selection of bugs 27

  28. Summary and take-aways We characterize I/O idempotence bugs, not addressed by prior systems, and find they exist in real code IBIS-S provides information to programmers about hard-to-reason about I/O dependences IBIS-D detects concrete bug instances when running on real energy-harvesting hardware I/O Dependent Idempotence Bugs in Intermittent Systems Milijana Surbatovich, Limin Jia, Brandon Lucia 28

Related


More Related Content

giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#