JM233333's Blog
  • Programming Languages

    • C
    • Python
  • Algorithms and Data Structures

    • Data Structure
    • Fundamental Algorithms
    • Graph Theory
  • GNU Toolchain

    • Bash
    • gdb
  • Development Environment

    • Ubuntu
    • QEMU
  • Development Tools

    • Git
    • VSCode
  • Operating Systems

    • Principles of Operating Systems
    • Xv6
    • Linux Kernel
  • Software Testing and Analysis

    • Software Testing
    • Software Analysis
    • Program Verification
  • LeetCode
  • XJTUOJ
  • System

    • System Performance
  • Programming

    • ...
  • Others

    • ...
  • Paper Reading

    • Model Checking
    • Fuzzing
    • Symbolic Execution
  • 3D Game Programming

    • 3D Mathematics

JM233333

弱小可怜又无助的学术废物
  • Programming Languages

    • C
    • Python
  • Algorithms and Data Structures

    • Data Structure
    • Fundamental Algorithms
    • Graph Theory
  • GNU Toolchain

    • Bash
    • gdb
  • Development Environment

    • Ubuntu
    • QEMU
  • Development Tools

    • Git
    • VSCode
  • Operating Systems

    • Principles of Operating Systems
    • Xv6
    • Linux Kernel
  • Software Testing and Analysis

    • Software Testing
    • Software Analysis
    • Program Verification
  • LeetCode
  • XJTUOJ
  • System

    • System Performance
  • Programming

    • ...
  • Others

    • ...
  • Paper Reading

    • Model Checking
    • Fuzzing
    • Symbolic Execution
  • 3D Game Programming

    • 3D Mathematics
  • Reading Papers 00 - Related Works
  • Reading Papers 01 - Model Checking
    • Distributed System
      • NSDI'09 - MoDist (to-be-readed)
      • SOSP'11 - DIR (to-be-reviewed)
      • OSDI'14 - SAMC
  • fuzzing

  • symbolic-execution

  • verification

  • Reading Papers 01 - Concurrency Testing
  • Reading Papers 02 - Crash Consistency
  • Reading Papers 10 - System Design
  • Reading Papers 20 - Others
  • others

  • FUCK-ELF
  • paper-reading
JM233333
2022-03-01
1096

Reading Papers 01 - Model Checking

Creative Commons

# Model Checking

# Distributed System

# NSDI'09 - MoDist (to-be-readed)

# SOSP'11 - DIR (to-be-reviewed)

dynamic interface reduction (DIR) 是模型检验的一种新的状态空间缩减技术。DEMETER 是实现了 DIR 技术的框架,基于该框架能够在已有的 model checker 中以合理的工作量实现 DIR 技术。

DIR 基于以下两个原则:

分别检查不同组件 :

使用良好定义的接口来封装软件复杂性是实践中常见的做法。基于这一点,model checker 可以认为被测软件系统是由一组 组件 (component) 构成的,每个组件都向软件系统的其它部分提供一组良好定义的接口。

更一般地,所有导致一个组件影响到另一个组件的行为(例如共享内存,failure correlatons ,或其它隐式通道)都由 接口行为 (interface behaviour) 捕获。除接口行为外的其它行为都是包含在局部状态空间内的。

组件之间通过 接口对象 (interface object) 进行交互,例如通信通道或共享对象等。 给定每个组件的接口行为,DIR 可以分别检查每个组件的局部状态空间,尽可能避免对全局状态空间进行不必要的搜索。

动态地发现接口行为 :

DIR 真实地运行目标组件,并在状态空间的探索过程中动态地发现各组件的接口行为。

# OSDI'14 - SAMC

利用 white-box 的信息作为指导以删减冗余的事件交错,即根据分布式系统中各节点对 message 的处理方式,判定 message 之间的依赖关系,并避免枚举 independent message 之间的交错。

基于四种 semantic-aware 的删减策略,由测试人员补全 protocol-specific 的谓词函数 ppp 。

  • Local-Message Independence (LMI) : Discard, Increment, Constant, Modify

  • Crash-Message Independence (CMI) : Global/Local Impact

message event vs crash/reboot event :前者只能删减冗余的事件交错,但后者是 model checker 引入的,因而如不必要则可删减事件本身。

  • Crash Recovery Symmetry (CRS) :不同节点的崩溃可能引起 symmetrical 的 recovery 行为,即产生相同的 message 并以相同的方式改变节点的局部状态。从节点的实现中提取影响 recovery 行为的 if 分支,据此在插入 crash event 之前推断如果 crash 将会发生何种 recovery ,维护已执行的 recovery history 并跳过不必要的 crash event 。

  • Reboot Synchronization Symmetry (RSS) :类似于 CRS 。

#Research#Paper Reading#Model Checking

← Reading Papers 00 - Related Works Reading Papers - Fuzzing Overview→

最近更新
01
Linux Kernel 00 - Introduction
08-01
02
Linux Kernel 01 - Build and Run a Tiny Linux Kernel on QEMU
08-01
03
Linux Kernel 01 - Debug the Linux Kernel
08-01
更多文章>
Theme by Vdoing | Copyright © 2019-2022 JM233333 | CC BY-NC-SA 4.0
  • 跟随系统
  • 浅色模式
  • 深色模式
  • 阅读模式