seL4:一个大的内核锁已经足够
论文戳这里 ，公开演讲PPT戳这里
前情提要
seL4 是一个安全的嵌入式系统，只支持有MMU的开发板，现在的移动CPU也在堆核心，所以要研究是否用更细的锁来提高可扩展性（Scalability）。
论文
文章在研究了在IPC过程中引入更细致的锁对性能的影响。Peter在内核里面加了4个锁，这四个锁有两种实现方式，一种是用原来的实现方式，另一个是用Intel独有的ntel TSX指令集（图中x86 RTM的数据）。
可以看出用更多的锁会造成更多的性能损失，而且如果锁的争抢需要跨越物理的L2 Cache，那么将会损失更多的性能，甚至造成损失的性能超过一个IPC的时间。
这个图的解释是，如果要争抢一个跨越物理缓存界限的锁，那么这个信号将会需要100～200个时钟周期（cycle)。又如上图，我们只需要800个时钟完成一个IPC。我看到这里就想，锁是为了提高吞吐量，提高可扩展性的（并发程度），Peter也给出了他的数据，印证了我的想法。
如图所示，方格的在最底下的线是只用一个大锁的成绩，在x86上输得很惨。在ARM上多于4核会优于一个大锁的成绩。那么Peter对此的解释是现实的情况下，我们并不会有显著的区别。Peter 用的是 Yahoo! Cloud Serving Benchmark，一个云服务读写性能测试，测试的结果并没有很大的区别，甚至稳定性要比Linux好。而且，如果要加锁，现在的Isabelle/HOL是很难证明这个复杂逻辑的Sound Correctness（显式正确），毕竟他们还在努力证明多核心配置下的seL4的正确性。 Peter得出的结论是，普通的应用并不会因为系统调用而造成瓶颈。
想法
在一般程序的运行过程中，并不会经常产生系统调用，而最常用的系统调用IPC有特殊的优化，十分快。但是总有一种跑题了的想法萦绕在我的心头。锁的作用不就是提升吞吐量才引入操作系统内核的，越细致的锁可以带来更好的吞吐量，本身的研究也证明了这一点，那为什么还要强行说一个锁就够了，只是因为完全形式化证明所以加不了锁而已。
而不能说加锁这件事情没有必要吧，如果应用程序真的需要这么高的IPC吞吐量怎么办。而且是八个核心的吞吐量堆在这个大锁上面的时候怎么办。而且也不是每个系统调用都是这么的快，只要不是IPC fastpath（快速线程间通信），记得没错是2000cycle起跳，那么即使再快的IPC也要等另一个核心的系统调用完成。那么应用程序将会受到没法预知的IPC延迟，因为他本身预计的是一个快速的IPC，如果这个CPU有很多吵闹的邻居，IPC的抖动将会无法DEBUG，因为这是写在Specification（设计参数）里面的。而且Radius也是一个基本上是单核心的程序，这个宏观测试也没有应用到细致锁的性能。
Figure 3 shows mean throughput for varying number of cores. Standard deviations are shown as (except for Linux nearly indistinguishable) error bars.
The figure shows that throughput is independent of the kernel variant. Further investigation reveals that overall sys-tem throughput is limited by the network bandwidth, and that the all cores have significant idle time. (Page 6 in Paper)
这个测试既没有跑满CPU性能，也不是IPC限制的测试，也没有开发多核心性能（Radius主要是单核心性能，不太涉及多核心，也不会因为IPC性能影响)。所以这个宏观测试是对但是无效的测试，无法证明论点的正确性。
我对这个反直觉的事情调查了一下，发现2012年Gernot的一个PPT（戳这里）。
这里现实了如果超过八个核心，大部分的时间将会浪费在内核态，估计大部分的时间就是浪费在这个锁上面。这里说的Limit of shared L2 cache也是一件很难过的事情，因为现在的L2缓存都都是在一小部分核心共享的比如2个或4个核心之间，按照这两个PPT说的事情，如果要提高性能，那么每个L2缓存必须挂载一个独立的seL4核心，而这又会对传统的编成范式造成不小的挑战。
小总结
seL4选择一个大核心锁是一个无奈之举，因为形式化证明暂时还无法证明多核心涉及锁的有效性（已经有理论，需要等大佬应用到seL4里面）。现在在seL4的多核心实现也还只是个补丁。但是对于现在的嵌入式系统4核以下的情况，依旧有其一定的竞争力。