TLC Model Checkerとは形式仕様記述言語であるTLA+のモデル検査ツールです。TLA+で書かれた仕様の不変式のviolationやLivenessやSafety 特性のviolationの検出などをしてくれます。
そんで、このTLC Model Checkerというのは、CUIで使えたほうが便利だと思うんですよね。実はTLA+にはTLA ToolboxというIDEがあって、GUIからマウスポチポチで呼び出して検証することもできるのですが、仕様検証という作業は（仕様規模によりますが）すごいCPUパワーとストレージを食います。
[xxx@host:~/xxx/tla+/raft]$ tlc -config SPEC.cfg ./first.tla
TLC2 Version 2.14 of 10 July 2019 (rev: 0cae24f)
Running breadth-first search Model-Checking with fp 82 and seed 1539151492344761609 with 1 worker on 24 cores with 21424MB heap and 64MB offheap memory (Linux 3.10.0-862.9.1.el7.x86_64 amd64, Oracle Corporation 1.8.0_181 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/xxx/xxx/tla+/raft/first.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/FiniteSets.tla
Parsing file /tmp/Sequences.tla
Parsing file /tmp/TLC.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module first
Starting... (2020-02-13 11:51:47)
Error: TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.NullPointerException
java.lang.NullPointerException
at tlc2.tool.impl.SpecProcessor.processSpec(SpecProcessor.java:346)
at tlc2.tool.impl.SpecProcessor.<init>(SpecProcessor.java:157)
at tlc2.tool.impl.Spec.<init>(Spec.java:121)
at tlc2.tool.impl.Tool.<init>(Tool.java:126)
at tlc2.tool.impl.Tool.<init>(Tool.java:121)
at tlc2.tool.impl.Tool.<init>(Tool.java:116)
at tlc2.TLC.process(TLC.java:930)
at tlc2.TLC.main(TLC.java:247)
Finished in 00s at (2020-02-13 11:51:47)
class RPC(target: String) {
def send(msg: String): Unit = {
println(s"sent! ${msg} to ${target}\n")
}
}
class RPCBinder(rpc: RPC) {
def send(msg: String): Unit = {
rpc.send(msg)
}
}
trait Base {
val rpc: RPC
val binder: RPCBinder = new RPCBinder(rpc)
}
trait BaseDefault { base: Base =>
val rpc = new RPC("Node0")
def sendHello(): Unit = {
binder.send("Hello")
}
}
trait BaseFunc1 { base: Base =>
def sendFunc1(): Unit = {
binder.send("Func1")
}
}
class BaseMode1 extends Base with BaseDefault with BaseFunc1 {
def doSend(): Unit = {
sendHello()
sendFunc1()
}
}
object Main {
def main(args: Array[String]){
println("start!!")
val base = new BaseMode1()
base.doSend()
println("end!!")
}
}
[thoth@~/programs]$ scala bbbb.scala
start!!
java.lang.NullPointerException
at RPCBinder.send(bbbb.scala:9)
at BaseDefault.sendHello(bbbb.scala:21)
at BaseDefault.sendHello$(bbbb.scala:20)
at BaseMode1.sendHello(bbbb.scala:31)
at BaseMode1.doSend(bbbb.scala:33)
at Main$.main(bbbb.scala:42)
at Main.main(bbbb.scala)
家庭環境のNASで10GbEなぞ必要なのか？と訝しがる人がいるかもしれません。しかし、今どきの高速なNVMe SSD、具体的にはSamsungSSD 970 EVO Plusなどですと、シーケンシャルライトで2.4GB/secぐらいの速度はふつーにでます。RAIDを組めばもっと速度は出るでしょう。これはすでに1Gbpsを優に超える速度です。
ここで紹介したM/Bとケースと電源の構成ですと、ザワードのATX電源コネクタがM/Bに届かないのでATXの電源延長ケーブル（部品表7）を別途用意する必要があります。また、この電源は4pinのペリフェラル電源が一つしか出てません。U-NASNSC-810A Server Chassisは外部ファンで一つ、SATAのバックポート電源で一つ。計2つのペリフェラル4pin電源コネクタが必要なので、変換コネクタ（部品表8）が別途一つ必要です
結果、一応Windowsのデバイスマネージャー上ではIntelのEthernet Server Adapter X520-1として認識してますし、ドライバもIntelの公式のものが使えます。また、iperfで負荷を10分間連続してかけ続けてみても、概ね9Gbit/secの速度で通信しつづけてくれます。途中で劇的に速度低下したり落ちたりする様子はありません。スイッチ、NICともに問題ないようです。
を使いましょう。Ubuntu for Linuxのiperfはめっちゃ遅いです。9Gbit/secも出ません。I/Oエミュレーションレイヤーが遅いのかな？なんかWSLはI/O周りが遅い感じがしますよね。とはいえ、上のwindows版のiperfもcygwinのdllが同梱されてるんで…条件はWSLと同じだと思うんですがね…
