对《Presburger Formulas and Polyhedral Compilation》做一个总结。
这是一本由isl和PPCG的作者Sven Verdoolaege写的关于多面体编译的入门小册子。主要介绍了多面体编译相关的基础知识（数学基础-凸优化/编译基础-依赖分析）。在实践层面则使用PPCG这种isl-based的编译器——尽管isl不能和多面体编译划等号，但已成为多面体编译事实上的标准库。
Polyhedral Compilation通过一系列的program analysis/compilation techniques对程序中的语句实例dynamic-execution instances进行分析。
对一个并行编程模型做优化，其约束应该怎么处理呢？
比如openMP只是共享内存下的SIMT模型——在合适的地方加上#pragma，其他的交给编译器来做即可。编译器检测代码和数据之间的依赖关系，然后做线程级别的并行化，但他不会检测线程之间的data-race condition，故很大程度上取决于你的coding能力。
再比如MPI则是靠进程间通信IPC来完成数据交换，对于一个分布式系统来说，通信开销和节点之间的data locality是一个很值得考虑的优化选项。
上周的研究生复试终于结束了，想起来真是做梦一样。
准备复试的过程中一直在看赵博士的《多面体编译理论与深度学习实践》这本书，两个月看完。发现自己对并行计算和编译器在并行性局部性挖掘方面的理解又深入了一点点。好处是终于有大把的时间来做想做的事情，又很担心学过的东西不成体系。
PPCG和Pluto都是面向polyhedral模型的source-to-sourcee编译器，前者支持OpenMP/CUDA/OpenCL代码生成，后者支持OpenMP代码生成。我不知怎么的就得出结论——想搞好编译器就要学好并行计算，那搞编译器的人是不是可以归到体系结构HPC这一波？我觉得差不多吧。
现阶段的HPC离不开CUDA，就像西方离不开耶路撒冷。
最近终于有时间研究一下MIT的神课6.824。
这门课教Distributed System，即多台物理隔离的计算机通过网络来协调，共同完成一致性任务，可以是计算任务，也可以是存储任务。
分布式系统和单机相比，除了有很多高并发的Partial Failures，更多的是硬件老化，断电，网卡失灵等这种现实问题。因此设计低成本高性能系统以及处理并发和网络问题——Performance性能和Fault Tolerance容错是这门课的核心。
课程共有20个Lectures和4个labs。和6.828一样重视实践——看论文，查资料，做lab~简单粗暴。所以学习过程基本上就按照如下推进：
Lecture要求的papersLectureslab相关的学习资料lab之前做6.828的时候就发现我在做这种学习过程很长，思考内容又很深的课程训练时很容易钻牛角尖而让自己乱了节奏，思维如若不能放松下来效果肯定不会太好——希望这次能尽量调整过来。
Type system的基本目的是防止在程序运行时发生execution error。这种Informal statement非形式化描述有很多内涵：首先该如何严格定义execution error；其次在这种定义下，描述absence of execution error也是Type system很nontrivial的性质——当PL .aka. programming language的所有运行时行为都能确保这种性质的话，我们就说该语言是type sound的。事实证明为了更加没有歧义的描述PL的type soundness，需要做大量的分析和证明。因此针对Type system的分类，描述和研究过程逐渐演变成为一套formal discipline即形式化体系。 \[
\frac{\Gamma_{1} \vdash \Im_{1} ... \Gamma_{n} \vdash \Im_{n}}{\Gamma \vdash \Im}
\]
The formalization of Type system需要一套精确的符号和定义系统，一个严格正确的Type system可以对语言定义的各个重要性质进行完整的判断。而非形式化的描述甚至做不到完整概括语言的type structure则更谈不上实现上的唯一性。比如不同的编译器对于同一套语言Type system的实现往往不尽相同，甚至有一些type unsound的语言定义导致一段代码明明通过typechecker的检查但在运行时奔溃掉。理想情况下我们说formal Type system应该是所有typed programming languages内核定义的一部分。这样的话，typechecking算法就可以严格按照精确的类型spec执行，从某种程度上该语言可以看成是Type sound的。
Tai-e是一个程序分析框架 By谭添老师。共有8个实验，包括：
这里复盘实验中遇到的各种坑，包括对分析算法实现细节上的理解，甚至Java语言本身的特性。
在IFDS出现之前，经典intra-procedural analysis框架(D,L,F)对于程序分析问题的研究还停留在①多项式时间处理specific individual problem比如constant propagation/pointer analysis②多项式时间处理locally separable proble（经典bit-vector/gen-kill问题——reaching definitions,available expressions,live variabl的过程间分析）③对普遍分析问题提供非多项式时间的算法方案。
随着POPL'1995发表的Precise Interprocedural Dataflow Analysis via Graph Reachability通过将一类inter-procedural analysis问题转化为a special kind of graph-reachability problem图可达性问题——IFDS框架横空出世。IFDS除了针对separable problems，还针对包括truly-live variables,copy constant propagation,possibly-uninitialized variablestruly-live variables在内的non-separable problems等一大类普遍性分析问题都提供了多项式时间的精确解决手段。由于IFDS本身的约束，作者在Theoretical Computer Science'1996上还发表过一篇Precise interprocedural dataflow analysis with applications to constant propagation提出IDE框架来处理interprocedural constant propagation等IFDS框架处理不了的non-distributive问题。这两篇论文为程序分析领域引入新的血液。
近年Sparse Value IFDS,Disk-Assisted IFDS等课题一直是学术界的研究热点。在工业界比如phasar等程序分析工具中IFDS/IDE也有具体实现。