分布式系统学习——NVM-Level-Hash实验 Level-Hash 编译遇到问题 123456789[edwardzcn@h1 10:18:28 persistent_level_hashing]$makegcc -c test.cIn file included from level_hashing.h:10:0, from test.c:1:log.h:9:73: fatal error: .../qua 2020-07-17 Computer Science 分布式系统 分布式系统 NVM
《我执》读书笔记 我执 P006 “《我执》写的，正是一种极度强烈的‘有我’的文学；《我执》记录的，正是唯有透过这种‘有我之境’才会出现的奇异景致。” P014 “《我执》有浓厚的忏悔录风格，哪里来自奥古斯丁哪些来自卢梭，无法一一细表。” 八月一日 题解 P003 “我知道了；这一切谎言与妄想，卑鄙与怯懦。它们就像颜料和素材，正好可以涂抹出一整座城市，以及其中无数的场景和遭遇。你所见到的，只不过 2020-07-16 Life 阅读 阅读
操作系统学习——知识点复习整理提纲 计算机系统概述 操作系统地体系结构 大内核和微内核 操作系统体系结构，关于操作系统在核心态应该提供什么服务、怎样提供服务？有关这一问题的回答形成了两种主要的体系结构：大内核（单一内核）和微内核。 大内核系统将操作系统的主要功能模块都作为一个紧密联系的整体运行在核心态，从而为应用提供高性能的系统服务。因为各管理模块之间共享信息，能有效利用相互之间的有效特性，所以具有无可比拟的性能优势。 但 2020-07-11 Computer Science 操作系统 操作系统
Coq学习——FRAP阅读笔记Chap12 CHAPTER 12 Hoare Logic: Verifying Imperative Programs 从上一章节两个维度前进一步。 从函数式转为命令式语言 回到对深度一致性（deep correctness）性质的证明，而非缺乏类型相关的崩溃 尽管如此，基本的证明结构最终还是一样的，因为我们再一次证明了转移系统的不变量（invariants of transition sys 2020-07-11 Computer Science 形式化验证 形式化验证
Coq学习——FRAP阅读笔记Chap4 CHAPTER 4 Semantics for Arithmetic Expressions via Finite Maps 为了解释章节 2 中数学表达式的含义。我们需要一个表示每个变量值的方法。使用finite maps（有限映射），顾名思义，有限域，可通过\(m[k \mapsto v]\)进行拓展，注意得到还是一个 map。符合下面的基本公理 \[\dfrac{}{m[k \maps 2020-07-11 Computer Science 形式化验证 形式化验证