Model Checking of Multi-Process Applications Using SBUML and GDB

Please download to get full document.

View again

All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Information Report
Category:

General

Published:

Views: 8 | Pages: 0

Extension: PDF | Download: 0

Share
Related documents
Description
Model Checking of Multi-Process Applications Using SBUML and GDB. Yoshihito Nakagawa* (University of Tokyo) Richard Potter ( Japan Science and Technology Agency ) Mitsuharu Yamamoto (Chiba University) Masami Hagiya** (University of Tokyo) Kazuhiko Kato (Tsukuba University). *NAMCO.
Transcript
Model Checking ofMulti-Process Applications Using SBUML and GDB Yoshihito Nakagawa* (University of Tokyo) Richard Potter (Japan Science and Technology Agency) Mitsuharu Yamamoto (Chiba University) Masami Hagiya** (University of Tokyo) Kazuhiko Kato (Tsukuba University) *NAMCO **Speaker Background
  • Model checking
  • Verification of concurrent systems
  • Systematic exploration of the state space
  • E.g., ensure no deadlock occurs
  • Focus on verification of program code
  • SLAM[Ball et al 01], Blast[Henzinger et al 03]
  • Verisoft[Godefroid 97], CMC[Musuvathi et al 02]
  • Our Goal
  • Real-environmental model checking
  • Use of OS resources (e.g., file system)
  • Flexible control of the granularity of scheduling
  • Evaluation of practicality by sample applications
  • Issues:
  • Provide real execution environment
  • Control nondeterminism in execution order
  • Traverse all nondetermistic choices
  • Method
  • SBUML + GDB
  • Real execution environment
  • Virtual machine technology
  • Control nondeterminism
  • Breakpoints in debugger
  • Traverse all nondeterminstic choices
  • Backtracking by saving/restoring execution states of virtual machine
  • Implementation of model checker by Ruby1.8.1
  • Internal/external monitor, GUI
  • Verification of concrete sample applications
  • Dining philosopher, Remote agent experiment
  • Virtual Machine andUser-Mode Linux
  • Provide virtual (guest) OS on top of real (host) OS
  • Various implementations
  • VMWare, Virtual PC, Bochs, CoLinux, UML, Xen, LilyVM, …
  • Progress of CPU and growth of memory made them practicable
  • User-mode Linux (UML)
  • Extension to Linux kernel (by Jeff Dike)
  • Open source
  • Execute guest Linux on host Linux
  • ScrapBook for User-Mode Linux Host OS
  • Further extension to User-mode Linux
  • UML Scrapbook and Realization of Snapshot Programming Environment [Sato, Potter 03]
  • Script language support
  • Virtual machine ScrapBook for User-Mode Linux Host OS
  • Further extension to User-mode Linux
  • UML Scrapbook and Realization of Snapshot Programming Environment [Sato, Potter 03]
  • Script language support
  • Virtual machine Overview of Model Checker SBUML GDB Process External Monitor Internal Monitor GDB Process GDB Process save/restore Target Application GDB SBUML GDB Process
  • Control process execution by breakpoints
  • Where the execution of a process may block
  • Where the computation result depends on the execution sequence of processes
  • External Monitor Internal Monitor GDB Process GDB Process save/restore Target Application Internal Monitor SBUML GDB Process
  • Which process can be resumed without blocking
  • Blocking condition, inspection function (given by hand)
  • Execution states of virtual machines
  • Program counters, blocking condition, shared variables
  • External Monitor Internal Monitor GDB Process GDB Process save/restore Target Application External Monitor SBUML GDB Process
  • Determine process that should be restored next
  • Depth-first search of the execution state space
  • Backtracking by saving/restoring execution states of virtual machines
  • External Monitor Internal Monitor GDB Process GDB Process save/restore Target Application Toy Example: Dining Philosopher Problem (a) Initial state (b) Deadlock
  • Each philosopher repeats to think and eat
  • Potential deadlock
  • N = 3 Verification while (1) { read(pipes[i%NUM].fd[0],&c,1);// (A) printf("%d takes his left fork...\n",i); read(pipes[(i+1)%NUM].fd[0],&c,1); // (B) printf("%d takes his right fork...\n",i); printf("%d waiting...\n", da->id); write(pipes[i%NUM].fd[1],&c,1); printf("%d leaves his left fork...\n",i); write(pipes[(i+1)%NUM].fd[1],&c,1); printf("%d leaves his right fork...\n",i); } int pipe_readable(int fd) { fd_set rfds; struct timeval timeout = {0, 0}; FD_ZERO (&rfds); FD_SET (fd, &rfds); return select(fd + 1, &rfds, NULL, NULL, &timeout); }
  • Code implemented by C
  • Philosopher as process, fork as pipe
  • Inspection function: User-defined (and added) function for verification Target Code: Task for each philosopher, Variable i … Philosopher ID Result
  • 8 states in total (1 deadlock)
  • Example:Remote agent experiment (RAX)
  • Software for spacecraft control
  • Developed by NASA Ames conjointly with JPL
  • Deadlock occurred during actual flight
  • Error identified from flight data
  • Challenge to formal method team
  • Verification with keeping the error cause secret
  • Error detection by Java Path Finder [Havelund, Lowry ’00]
  • Remote agent experiment (RAX) ! sleep sleep
  • Interaction between two processes
  • Each process repeats <wake up>, <sleep>
  • If a process in action get notification <wake up>, then skip the next <sleep>
  • Proc. 1 sleep sleep Proc. 2 sleep ! 1 sleep sleep 2 Target Code Fragments void *first_task(void *ev) { struct event *e1 = (struct event *)ev; struct event *e2 = e1+1; int count = 0; while (1) { if (count == e1->count) /* (A) */ sleep(e1); /* (B) */ count = e1->count; wake_up(e2); } } void *second_task(void *ev) { struct event *e1 = (struct event *)ev; struct event *e2 = e1+1; int count = 0; while (1) { wake_up(e1); /* (C) */ if (count == e2->count) sleep(e2); count = e2->count; } }
  • Possible deadlock (A)  (C)  (B)
  • Proc. 1 may overlook the <wake up> call by Proc. 2
  • Verification (1) void cond_wait(struct event *e) { static struct sembuf sop_dec_both[] = {{SEM_MUTEX, -1, 0}, {SEM_COND, -1, 0}}; static union semun {int val;} arg = {0}; e->waiting = 1; mutex_unlock(e); semop(e->semid, sop_dec_both, /* (i) */ sizeofarray(sop_dec_both)); e->waiting = 0; semctl(e->semid, SEM_COND, SETVAL, arg); } void mutex_lock(struct event *e) { static struct sembuf sop_dec_mutex[] = {{SEM_MUTEX, -1, 0}}; semop(e->semid, sop_dec_mutex, /* (ii) */ sizeofarray(sop_dec_mutex)); }
  • Where process may block
  • IPC semaphore operations
  • (i), (ii)
  • Blocking condition
  • (i) can_lock(e) == 0
  • (ii) can_resume(e) == 0
  • int can_lock(struct event *e) { return semctl(e->semid, SEM_MUTEX, GETVAL); } int can_resume(struct event *e) { return semctl(e->semid, SEM_MUTEX, GETVAL) && semctl(e->semid, SEM_COND, GETVAL); } Inspection function: User-defined (and added) function for verification Verification (2) void *first_task(void *ev) { struct event *e1 = (struct event *)ev; struct event *e2 = e1+1; int count = 0; while (1) { if (count == e1->count) /* (1) */ sleep(e1, count); count = e1->count; /* (2) */ wake_up(e2); } } void *second_task(void *ev) { struct event *e1 = (struct event *)ev; struct event *e2 = e1+1; int count = 0; while (1) { wake_up(e1); if (count == e2->count) /* (3) */ sleep(e2, count); count = e2->count; /* (4) */ } }
  • Where the result depends on the execution order
  • Access to shared variables {e1, e2}
  • (1)~(4)
  • Blocking condition always returns “false”
  • Never blocks here
  • Experimentation Result Result Specs Possible Application: “Mbox Locking Problem”
  • Several programs make access to a single mail spool
  • MDAs, POP/IMAP servers, MUAs
  • Different lock mechanisms
  • fcntl, flock, “dot-locking”
  • Some programs support them only partially
  • Danger of deadlock/livelock
  • Real environmental example
  • Shared resource in a file system
  • Related Works
  • Use of modified SBUML scheduler [Sato, Potter 03]
  • Lack of flexibility
  • Granularity in scheduling … per system call
  • Ad-hoc way to extract information about execution states
  • CMC [Musuvathi 02]
  • Verification by execution of event-driven program
  • Backtracking by saving/restoring global variables and heap
  • Verisoft [Godefroid 97]
  • Backtracking by re-execution from the initial state
  • Discussion A 2
  • Search strategy depends of the relation between:
  • restore time
  • execution time till the next breakpoint
  • B 1 C 1 : State ID : Process ID A Restore C => Resume 2 and Resume 1 Conclusion
  • Framework for real-environmental model checking
  • Verification of sample applications in “practicable” time
  • Flexible framework
  • Arbitrary granularity in scheduling
  • Current Limitations
  • User must specify some items
  • Breakpoints, blocking condition
  • Inspection function
  • Define execution states (hash values)
  • No multi-thread applications support
  • GDB cannot handle selective execution of threads reliably
  • Future Work
  • Automatic generation of items for verification
  • Static analysis of target program
  • Much more speed-up
  • Combination with re-execution
  • Execution on cluster machines
  • More complicated examples
  • Mbox locking problem
  • Recommended
    View more...
    We Need Your Support
    Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

    Thanks to everyone for your continued support.

    No, Thanks