在CS510 Software Engineering的课上说到了Weak Fairness和Strong Fairness. 以前meeting的时候提到过这个概念，但是当时没听懂.. 复习的时候自己想出一个自洽的解释了，赶快记下来！

Update 10/07/2015: Add descriptions of weak/strong fairness from paper The Temporal Logic of Actions.


CHESS

课上介绍到Concurrent Testing的时候举了CHESS作为例子，slides见这里。

CHESS是一个测试/重现concurrency bugs的工具。这个concurrency bugs有时被称作heisenbugs, 意指测不准的谐音梗。我一直觉得谐音梗玩多了会显得LOW, 但这个梗用的真是棒！Heisenbugs指的是那种，时不时出现暴露一个bug, 但是一旦想要定位它，比如通过添加printf()等调试语句，bug就消失了.. ╮(╯_╰)╭

CHESS能够重现这些bug, 它相当于是个user mode scheduler, 把所有的interleaving都试一遍就知道哪些情况会有bug了.. 所以我感觉又是一个执行的越久，就能多测一点的工具。在没有全部验证过的时候，无法保证一定是没有错误。另外CHESS的主打就是concurrency bugs, 普通bugs不是它的发力点。还有，因为这是MSR做的东西，所以是支持Win32和.NET

关于CHESS的细节就不多写了，在这篇paper里。接下来主要是说一说CHESS中涉及到本文标题的那些东西。

CHESS Scheduler

CHESS就是每次跑一个新的scheduling, 然后在其间检测

  • Assertion violations
  • Deadlocks
  • Data races
  • Livelocks

等等。而CHESS Scheduler就是要遍历所有的可能，给出所有的scheduling去执行。在slides中看到CHESS甚至有考虑到relaxed memory model的non-determinacy, 碉堡了！虽然不知道细节..

每个thread内有很多个preemption point, 这些个preemption point之间就是一个个 “atomic block”. 然后CHESS在执行的时候从来都是单线程的，每次只执行一个thread, 到了一个preemption point的时候就停下来，让scheduler看看接下来是哪个thread了，从而模拟出多线程的效果（所以我更好奇他们这种模拟方式是怎么处理relaxed memory model的，不过没有认真看paper, let it go吧..）。也因此，说CHESS是一个user model scheduler.

根据作者们的观测，大部分的concurrency bug都能在2次preemption的情况下就出现，在只考虑2次preemption的情况下，复杂度就没有原本exponential那么吓人了！

Fairness

CHESS在遇到loop的时候也是会unroll的，要unroll就得有个depth bound, 不然可能无穷无尽unroll下去。这样unroll会造成一些问题，其中一个就是无法找到livelock. 这里就涉及到livelock, fairness等一串概念了。

Deadlock想必每个人都听过，Livelock指的是类似的东西。类比地说，deadlock是每个人都无路可走，而livelock是并非无路可走、但是最终只是绕圈圈，没有实际进展。

Livelock对应的是一个 “liveness”的概念，liveness与safety相对应，safety property指的是don’t do anything bad, liveness property指的是do something good, 有progress!

// 我的14年下半年就一直在做和liveness相关的东西，但其实做的很痛苦.. 因为一直碰壁 >_<

要讨论liveness, 就需要有fairness, 即本篇的关键词。假如你无法保证整个scheduler的fairness, 有些thread可能永远执行不到，那谈论这个thread上的一些assertion是否迟早为true又有什么意义呢。

Weak / Strong Fairness

根据slides上的定义，Weak Fairness指的是：

A thread that remains enabled should eventually be executed.

根据我的理解（与猜测），有可能是先有了weak fairness对应的实现，再有了这样一个概念。普通的round-robin实现的就是weak fairness. 一个thread知道自己在round-robin中是一定会被执行到的，只要不出什么变动。

WEAK这个词我是这么理解的：

  • 首先，使用了round-robin scheduling, 那么当前的一个enabled thread是一定会被执行到的，所谓eventually executed.
  • 但是，一旦这个thread在马上就要被执行到的时候变成了disabled, 如等待的一个空lock突然被别人抢了，此时这个thread变成了disabled, 就不需要保证eventually executed了。
  • 而一旦过了这个thread, 那个lock又空出来了，thread又变成了enabled状态，于是再次eventually executed.
  • 这样循环往复，就可能造成，虽然是weak fairness, 但是某个thread永远无法执行到的情况，是所谓WEAK.

整个逻辑是如此的自洽，以至于我坚信是先有了真正round-robin的实现，发现了这个问题，才提出的weak fairness的概念..

相对应的，Strong Fairness指的是：

A thread that is enabled infinitely often is scheduled infinitely often.

定义很绕，但其实strong fairness就是去除了这种某个thread可能永远执行不到的情况。它的实现可以很简单，就是round-robin + priority. 一直执行不到的thread会增加优先级，从而下次它一被enabled, 就可以被执行到。


Update 10/07/2015: From TLA paper:

Weak fairness asserts that an operation must be executed if it remains possible to do so for a long enough time. “Long enough” means until the operation is executed, so weak fairness asserts that eventually the operation must either be executed or become impossible to execute—perhaps only briefly. A naive temporal logic translation is

1
weak fairness: (◇ executed) ∨ (◇ impossible)

Strong fairness asserts that the operation must be executed if it is often enough possible to do so. Interpreting “often enough to mean infinitely often, strong fairness asserts that either the operation is eventually executed, or its execution is not infinitely often possible. Not infinitely often possible is the same as eventually always impossible (because (7) implies ¬□◇ … ≡ ◇□¬ …), so we get

1
strong fairness: (◇ executed) ∨ (◇□ impossible)

These two temporal formulas assert fairness at “time zero”, but we want fairness to hold at all times. The correct formulas are therefore

1
2
weak fairness: □((◇ executed) ∨ (◇ impossible))
strong fairness: □((◇ executed) ∨ (◇□ impossible))

Temporal logic reasoning, using either the axioms in Section 5.6 or the semantic definitions of ❑ and O, shows that these conditions are equivalent to

1
2
weak fairness: (□◇ executed) ∨ (□◇ impossible)
strong fairness: (□◇ executed) ∨ (◇□ impossible)

Fair Cycle

现在定义都说完了，回到这一章的最开始，说CHESS要unroll loop, 但是unroll会造成一些问题，如无法找到livelock. 那么CHESS是怎么处理的呢？这就说到了fair cycle的概念，在slides的第34页。

slides上非常的言简意赅：

  • All cycles in correct programs are unfair.
  • A fair cycle is a livelock.

这两句话我纠结了好久，最后是这么想通的：

  • 怎样算是livelock呢？就是那种虽然看着有进展，但是实际上在原地踏步的。

  • 怎样算是fair呢？就是有跳转到其它states去的，像slides里说的那种在 淡蓝色 “!done” states内部跳转的，这种算是unfair, 在correct programs中，cycles都应该是这种的。

  • 但是在有livelock的program中，若看着是fair, 并跳转到其它states里去了，但是最终仍旧是一个cycle, 在原地踏步，这就是一个livelock!

所以，CHESS首先不会去unroll an unfair cycle (源paper里的说法是最多unroll 2次), 因为unroll出来也是探索过的state, 从而更加高效。

其次，CHESS会去detect fair cycle, 然后就可以找到livelocks.

就是这样，喵


碎碎念

之前在4/27, 我一时爽更新了hexo的版本，之前一直用的是2.x的版本，现在是3.x了，结果重新设置花了好一会儿，而且发现代码引用的格式都变了…. 似乎不再是等宽字符了的样子？

这周15 spring学期已经结束了，CS510 Software Engineering这门课程也已经结束了。我最开始上这门课的目的是为了多了解model checking的，也早就超额完成目标了，还写了好几篇博客存档，LLVM经验条也涨了一大大截！棒棒哒！

不过也留了好几个坑，abstraction interpretation还没有科普，还有symbolic execution & model checking的对比也还没有写，最后原本打算写的这门课的总结也没有写的欲望.. 暂时先let it be吧.. 慢慢有机会再填（真的会吗→_→）。快滚去research啊！！