Counting, Enumerating, and Sampling of Execution Plans in a Cost-Based Query Optimizer
最近补了一些优化器相关的背景知识，今天分享一篇论文Counting, Enumerating, and Sampling of Execution Plans in a Cost-Based Query Optimizer.pdf (sigmodrecord.org)。这个paper基于Volcano和Casca...
Recent Posts
Differences between SMR mechanisms
Hazard pointer vs shared_ptr
写在2023年春节前
每次想要说些什么，但在动笔时总是苍白无力。
Hazard pointer, part II
能否有足够工程能力将理论算法变现？
Hazard pointer, part I
断更太久，实在是最近太忙… 焦头烂额ing
Snapshot Isolation in TLA+
坦率来说，这次入坑TLA+的主要目的就是为了能够试着验证快照隔离。啃了大半本Practical TLA+，看了不少其他人的例子，自己也尝试写了些spec，仍然只能说勉强入门了。在网上能找到的大多数事务相关的spec都是TLA+直接实现的，目前对于我来说未免还是太困难了点。因此这篇文章，会通过TLA+的伪代码语言P...
Conflict Serializability and View Serializability
最近在看SnapshotIsolation的形式化验证，学习到了两个新概念Conflict Serializability和View Serializability。回顾下可串行化：多个事务执行的结果和这些事务按某种串行执行的结果相同。然后我们分别看下这两种串行化的概念。
2PC in TLA+, step 3
面对真实的世界…
2PC in TLA+, step 2
在上一篇里我们实现了一个最简单的2PC，其中无论RM还是TM都不会crash。在这一篇中我们会引入RM随时可能crash的情形，看看需要对2PC的实现进行多少修整。
2PC in TLA+, step 1
2PC广泛运用于各种分布式系统，然而就是这样一个看似平平无奇的算法，想要正确实现，绝不是一件容易的事情。这个系列应该会陆续写三篇，第一篇主要会在TLA+中描述一个简单的2PC算法。