上海交通大学：并发理论（PPT课件诗篇）Concurrency Theory

Concurrency Theory Xiaoju Dong(董笑菊) Joint course with prof. YUxi Fu(傅育熙) BASICS, Shanghai Jiao Tong University xjdong@sjtu.edu.cn http://basics.sjtu.educn/nxiaoju/concur17

Xiaoju Dong(董笑菊) Joint course with Prof. Yuxi Fu(傅育熙) BASICS, Shanghai Jiao Tong University xjdong@sjtu.edu.cn http://basics.sjtu.edu.cn/~xiaoju/concur17 Concurrency Theory

可题1 公安机关正在调查一宗盗窃案,现获得事实如下 A或B盗窃了文物 若A盗窃了文物,则作案时间不可能在午夜前 若B证词正确,则在午夜前屋里灯光未灭 若B证词不正确,则作案时间发生在午夜前 午夜时屋里灯光灭了 试问谁是盗窃犯? 2021年1月27日星期三 BASICS

问题1 公安机关正在调查一宗盗窃案，现获得事实如下： ◼A或B盗窃了文物 ◼若A盗窃了文物，则作案时间不可能在午夜前 ◼若B证词正确，则在午夜前屋里灯光未灭 ◼若B证词不正确，则作案时间发生在午夜前 ◼午夜时屋里灯光灭了 试问谁是盗窃犯？ 2021年1月27日星期三 BASICS 2

可题1 公安机关正在调查一宗盗窃案,现获得事实如下 A或B盗窃了文物 若A盗窃了文物,则作案时间不可能在午夜前 若B证词正确,则在午夜前屋里灯光未灭 若B证词不正确,则作案时间发生在午夜前 午夜时屋里灯光灭了 试问谁是盗窃犯? 命题逻辑 2021年1月27日星期三 BASICS

问题1 公安机关正在调查一宗盗窃案，现获得事实如下： ◼A或B盗窃了文物 ◼若A盗窃了文物，则作案时间不可能在午夜前 ◼若B证词正确，则在午夜前屋里灯光未灭 ◼若B证词不正确，则作案时间发生在午夜前 ◼午夜时屋里灯光灭了 试问谁是盗窃犯？ 2021年1月27日星期三 BASICS 3 命题逻辑

问题2 电灯开关 两个开关A、B同时控制一盏灯C (1)只要有一个开关处于开启状态灯就会亮 (2)只有两个开关之一处于开启状态灯才亮 请具体列出灯C在开关A和B处于什么情况 下会亮

问题2 电灯开关 两个开关A、B同时控制一盏灯C, (1) 只要有一个开关处于开启状态灯就会亮 (2) 只有两个开关之一处于开启状态灯才亮 请具体列出灯C在开关A和B处于什么情况 下会亮

问题2 电灯开关 两个开关A、B同时控制一盏灯C (1)只要有一个开关处于开启状态灯就会亮 (2)只有两个开关之一处于开启状态灯才亮 请具体列出灯C在开关A和B处于什么情况 下会亮 数字逻辑

问题2 电灯开关 两个开关A、B同时控制一盏灯C, (1) 只要有一个开关处于开启状态灯就会亮 (2) 只有两个开关之一处于开启状态灯才亮 请具体列出灯C在开关A和B处于什么情况 下会亮 数字逻辑

Formal methods In computer science, specifically software engineering and hardware engineering formal methods are a particular kind of mathematically based techniques for the specification development and verification of software and hardware systems The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines performing appropriate mathematical analysis can contribute to the reliability and robustness of a design. 2021年1月27日星期三 BASICS

Formal Methods ◼ In computer science, specifically software engineering and hardware engineering, formal methods are a particular kind of mathematically based techniques for the specification, development and verification of software and hardware systems ◼ The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design. 2021年1月27日星期三 BASICS 6

Formal methods Formal methods are best described as the application of a fairly broad variety of theoretical computer science fundamentals, in particular logic calculi, formal languages automata theory, discrete event dynamic system and program semantics but also type systems and algebraic data types to problems in software and hardware specification and veritication 2021年1月27日星期三 BASICS

Formal Methods ◼ Formal methods are best described as the application of a fairly broad variety of theoretical computer science fundamentals, in particular logic calculi, formal languages, automata theory, discrete event dynamic system and program semantics, but also type systems and algebraic data types to problems in software and hardware specification and verification 2021年1月27日星期三 BASICS 7

Concurrency a In computer science concurrency is a property of systems several computations are eXecuting simultaneously and potentially interacting with each other

9 Concurrency ◼ In computer science, concurrency is a property of systems ◼ several computations are executing simultaneously ◼ and potentially interacting with each other

Concurrency Computation any type of calculation use of computer technology in information processing(e.g. query in a database) (electronic)computers, quantum computers, DNA computers molecular computers etc a process following a well-defined model expressed in an algorithm, protocol, etc

10 Concurrency ◼ Computation ◼ any type of calculation ◼ use of computer technology in Information processing (e.g. query in a database) ◼ (electronic)computers, quantum computers, DNA computers, molecular computers, etc. ◼ a process following a well-defined model expressed in an algorithm, protocol, etc

Concurrency Interaction(or communication) Hand-shaking(synchronization) Value-passing Name-passing Process-passing 11

11 Concurrency ◼ Interaction (or communication) ◼ Hand-shaking (synchronization) ◼ Value-passing ◼ Name-passing ◼ Process-passing ◼ ……