Amdahl's Law
\[ Speedup = \frac{\text{1-thread execution time}}{\text{n-thread execution time}} \\ = \frac{1}{1 - p + \frac{p}{n}} \]
其中 p 是并发执行的代码在所有代码中的比例。
Safety & Linvness 安全性和活跃性
liveness 在中文版教材中被翻译为演进条件。
Safety vs. liveness
Safety: nothing "bad" will ever happen
Liveness: something "good" will happen eventually (but we don't know when)
Safety vs. liveness for sequential programs
Safety: the program will never produce a wrong result ("partial correctness")
Liveness: the program will produce a result ("termination")
Safety vs. liveness for state-transition graphs
Safety: those properties whose violation always has a finite witness ("if something bad happens on an infinite run, then it happens already on some finite prefix")
For any run R, R does not satisfy P iff there exists a prefix of R that does not satisfy P.
For any run R, R satisfies P iff every prefix of R satisfies P.
Liveness: those properties whose violation never has a finite witness ("no matter what happens along a finite run, something good could still happen later")
For any finite run R, there exists R1 such that R1 is an extension of R, and R1 satisfies P.
Safety: the properties that can be checked on finite executions
Liveness: the properties that cannot be checked on finite executions
(they need to be checked on infinite executions)
安全性：违反该属性时始终有有限见证者（“如果在无限运行中发生坏事，那么它已经发生在某个有限前缀上”）
对于任何运行 R，R 不满足 P，当且仅当存在不满足 P 的 R 前缀。
对于任何运行 R，R 满足 P，当且仅当 R 的每个前缀都满足 P。
活跃性：违反该属性时始终没有有限见证者（“无论在有限运行中发生什么，以后仍有好事发生”）
对于任何有限运行 R，存在 R1，使得 R1 是 R 的扩展，并且 R1 满足 P。
安全性：可以检查的属性有限执行
活跃度：在有限执行中无法检查的属性（需要在无限执行中检查）
Examples
| 属性 | 描述 | 类别 |
|---|---|---|
| Mutual exclusion | It cannot happen that both threads are in their critical sections simultaneously. 两个线程不可能同时处于临界区。 |
Safety |
| Bounded overtaking | Whenever thread A wants to enter the critical section, then thread B gets to enter at most once before thread A gets to enter. 每当线程 A 想要进入临界区时，线程 B 最多可以在线程 A 进入之前进入一次。 |
Safety |
| Starvation freedom | Whenever thread A wants to enter the critical section, provided thread B never stays in the critical section forever, A gets to enter eventually. 每当线程 A 想要进入临界区时，只要线程 B 不会永远停留在临界区中，A 最终就能进入。 |
Liveness |
| Deadlock freedom | When only A wants to enter the critical section, it gets to enter eventually. When both A and B want to enter the critical section, one of them gets to enter eventually. 当只有 A 想要进入临界区时，它最终可以进入。 当 A 和 B 都想要进入临界区时，其中一个最终可以进入。 |
Liveness |
