Specifying Systems 笔记2 Liveness & Fairness
+Specifying Systems 笔记2 Liveness
@@ -514,7 +515,7 @@
©
2017 -
- 2021
+ 2022
diff --git a/post/asciidoc-preview/diagram-classes-demo.svg b/post/asciidoc-preview/diagram-classes-demo.svg
index 46ccaa5..2cdbf82 100644
--- a/post/asciidoc-preview/diagram-classes-demo.svg
+++ b/post/asciidoc-preview/diagram-classes-demo.svg
@@ -1,29 +1 @@
-
\ No newline at end of file
+
\ No newline at end of file
diff --git a/post/asciidoc-preview/index.html b/post/asciidoc-preview/index.html
index 54b8a80..e2df212 100644
--- a/post/asciidoc-preview/index.html
+++ b/post/asciidoc-preview/index.html
@@ -55,7 +55,7 @@
-
+
@@ -160,6 +160,7 @@
\newcommand{\PICK}{\sc{PICK}}
\newcommand{\WITNESS}{\sc{WITNESS}}
\newcommand{\HIDE}{\sc{HIDE}}
+\newcommand{\@w}[1]{\textsf{``{#1}''}}
@@ -740,13 +741,13 @@ bibliography
显示某个引用
-A. Gidenstam, H. Sundell, and P. Tsigas, “Efficient Lock-Free Queues that Mind the Cache,” in 3rd Swedish Workshop on Multi-core Computing (MCC 2010), 2010.
+A. Gidenstam, H. Sundell, and P. Tsigas, “Efficient Lock-Free Queues that Mind the Cache,” 2010.
显示引用列表
-[1] A. Gidenstam, H. Sundell, and P. Tsigas, “Efficient Lock-Free Queues that Mind the Cache,” in 3rd Swedish Workshop on Multi-core Computing (MCC 2010), 2010.
+[1] A. Gidenstam, H. Sundell, and P. Tsigas, “Efficient Lock-Free Queues that Mind the Cache,” 2010.
@@ -759,18 +760,18 @@ Diagram by Coding
-
+
-
+
Figure 1. plantuml
-
+
Figure 2. graphviz
@@ -857,7 +858,7 @@ Diagram by Coding
©
2017 -
- 2021
+ 2022
diff --git a/post/dubbo-integrate-with-istio/index.html b/post/dubbo-integrate-with-istio/index.html
index 7417197..9dfe2be 100644
--- a/post/dubbo-integrate-with-istio/index.html
+++ b/post/dubbo-integrate-with-istio/index.html
@@ -160,6 +160,7 @@
\newcommand{\PICK}{\sc{PICK}}
\newcommand{\WITNESS}{\sc{WITNESS}}
\newcommand{\HIDE}{\sc{HIDE}}
+\newcommand{\@w}[1]{\textsf{``{#1}''}}
@@ -458,7 +459,7 @@ 参考资料
©
2017 -
- 2021
+ 2022
diff --git a/post/index.html b/post/index.html
index 2f04195..71f2c91 100644
--- a/post/index.html
+++ b/post/index.html
@@ -145,7 +145,7 @@ 2020
- Specifying Systems 笔记2 Liveness & Fairness
+ Specifying Systems 笔记2 Liveness
@@ -217,7 +217,7 @@ 2020
©
2017 -
- 2021
+ 2022
diff --git a/post/index.xml b/post/index.xml
index 676bbed..d9862d4 100644
--- a/post/index.xml
+++ b/post/index.xml
@@ -12,7 +12,7 @@
-
-
Specifying Systems 笔记2 Liveness & Fairness
+ Specifying Systems 笔记2 Liveness
/post/specifying-systems-notes-2/
Tue, 08 Sep 2020 21:00:00 +0800
@@ -20,12 +20,12 @@
<div id="preamble">
<div class="sectionbody">
<div class="paragraph">
-<p>Specifying Systems的1-7章层层推进，在实例中穿插着原理讲解，深入浅出地讲解了Specification是什么，以及如何规约系统设计。
+<p>Specifying Systems的1-7章层层推进，在实例中穿插着原理讲解，深入浅出地讲解了Specification是什么，以及如何设计系统规约。
这些Specification表明了系统的Safety属性 — 即系统行为被约束在一定范围内，不会做出一些不被允许的行为(something <strong>bad</strong> does not happen)。
在TLA+中，通常使用公式 \(Spec \triangleq Init \land \Box [Next]_{vars}\) 来描述系统的Safety属性(约束)。
-Safety属性说明了系统中什么不能发生，但无法表达系统中<strong>最终会发生</strong>的这类属性，而Liveness便可以表达("something <strong>good</strong> eventully happen")。
-Liveness使用时态逻辑公式进行描述，一个系统规约可以通过公式 \(Spec \triangleq Init \land \Box [Next]_{vars} \land F\) 来同时描述其对Safety和Liveness的要求，
-公式末尾的 $F$ 便是描述Liveness属性的公式。</p>
+Safety属性说明了系统中什么不能发生，但无法表达系统中<strong>某些时间一定会发生</strong>的这类属性，而Liveness便可以表达("something <strong>good</strong> eventully happen")。
+Liveness使用时态逻辑公式进行描述，一个系统规约可以通过公式 \(Spec \triangleq Init \land \Box [Next]_{vars} \land L\) 来同时描述其对Safety和Liveness的要求，
+公式末尾的 $L$ 便是描述Liveness属性的公式。</p>
</div></div></div>
diff --git a/post/latency-optimization-for-istio-proxy-based-on-envoy/index.html b/post/latency-optimization-for-istio-proxy-based-on-envoy/index.html
index bc35c54..c022218 100644
--- a/post/latency-optimization-for-istio-proxy-based-on-envoy/index.html
+++ b/post/latency-optimization-for-istio-proxy-based-on-envoy/index.html
@@ -161,6 +161,7 @@
\newcommand{\PICK}{\sc{PICK}}
\newcommand{\WITNESS}{\sc{WITNESS}}
\newcommand{\HIDE}{\sc{HIDE}}
+\newcommand{\@w}[1]{\textsf{``{#1}''}}
@@ -266,10 +267,10 @@ 架构简介
Istio在设计上分为了控制面和数据面。
控制面可以理解为各种配置管理和协调服务。比如，控制面自动从Kubernetes中提取Service信息，使用xDS协议将其下发到数据面，帮助数据面代理完成服务发现。
数据面完成各种具体的动作。如路由、熔断等流量管理，生成遥测信息进行上报，策略实施等。
-
+
图1: Istio架构示意图
数据面以sidecar模式实现，这是Istio为微服务带来强大能力却不用修改服务本身的关键：即在每一个服务实例旁，它都会运行一个envoy代理程序，将原来需要在服务内实现（如服务发现、负载均衡、监控追踪等）的功能移到独立进程中完成。
-
+
图2: 在Kubernetes平台上，Pod内增加了一个运行着envoy代理的容器，服务流量需通过envoy进行转发
注： 对于接下来的性能研究，文中出现的术语 proxy、sidecar、envoy可以视为同一个意思。
性能测试
@@ -309,7 +310,7 @@ 工具与方法
Coordinated Omission 问题
什么是Coordinated Omission？简单地说就是我们进行压测时，可能只是测量了「服务时间」，忽略了「排队等待时间」。而真实用户体验到的延时是「响应时间」，包含「服务时间」与「排队等待时间」两者之和。
-
+
(图中queue只是一种抽象，例如它可以来源于链路中的buffer，并发系统中的资源竞争等)
压测工具通常没有处理OC问题，它们大多定时发送一个请求，记录开始时间(begin_time)，然后接收响应并记录结束时间(end_time)，这样便得到一个请求的延时(end_time - start_time)。当新的发送周期到来时，继续发送下一个请求，记录延时，如此循环…
这种发包策略下当某个请求出现响应过慢，其响应时间点已经超过下一个发包周期开始时间点，导致压测工具延后了原本应该发送的请求，降低了实际测试RPS。最终，我们测量的数据中只有少部分请求的延时增加了（发生阻塞的那些请求），而真实环境中则可能有多个排队中的请求因为前面的请求阻塞而出现延时增加，用户体验到响应变慢的概率比压测环境报告的数据更大！
@@ -353,7 +354,7 @@ 自动化脚本
kustomization.yaml
kustomize 支持插件，某些操作内置的plugin无法完成，可以通过自定义plugin实现。
例如，下面的yaml格式内容描述了对istio-proxy容器进行添加initContainer、修改security、删除resource limits等操作。
-这些yaml内容使用的是json patch规范，在自定义的kustomize plugin中，我们将其转变为json格式之后，使用json-patch工具执行对istio-proxy容器配置的修改操作。
+这些yaml内容使用的是json patch规范，在自定义的kustomize plugin中，我们将其转变为json格式之后，使用json-patch工具执行对istio-proxy容器配置的修改操作。
- op: add
path: ${proxy_container_path}/securityContext/privileged
value: true
@@ -402,31 +403,31 @@ 自动化脚本
环境
测试环境使用5台8C16G节点的tke集群。istio-telmetry组件消耗的资源较多，服务端mixs消耗较多，1000QPS大概需要消耗1200m CPU，因此使用两个节点，以满足超过7000QPS的测试压力；pilot等其它控制面组件使用一个节点进行部署； nighthawk和mesh-mocker分别占用一个节点。自动化脚本打包在一个镜像中，每次在控制面组件所在节点运行。
测试中限制了nighthawk、mesh-mocker、envoy都使用2vCPU。同时，考虑到相同资源下，多核机器上worker线程数对并发度有直接影响，最终也会影响延时，因此我们对每个组件的工作线程数也限制为2。这样配置后，在OS调度下，几乎所有组件都是独立运行，不会互相影响，更容易评估使用Istio后envoy产生的影响。
-
+
Envoy打点
Istio数据面带来了明显的延时，把消息在链路中各个阶段的延时统计出来，是进行优化的重要依据。一开始我们思考利用内核态工具如bpftrace进行分析，但请求消息在envoy中进行了多次转发，内核态很难追踪应用层会话，统计时间并不方便，因此我们决定在envoy内部打点记录时间，测试结束后通过离线脚本计算消息在envoy中进行处理的延时。
-
+
client请求server是，每条消息Request依次经过envoy中的3，4，5，6几处，通过readv和writev系统调用读取或发送消息，Response以相反的顺序经过envoy。
我们将Request经过打点位置的时间戳记录为t(*)，将Response经过的时间戳记录为t'(*)，则一条消息在两个sidecar(envoy)中消耗的时间总计为：t(4)-t(3) + t'(3)-t'(4) + t(6)-t(5) + t'(5)-t'(6)。
为了防止打点带来过多的额外损耗，时间戳直接记录在预分配的连续内存（数组）中，如果使用1w QPS测试10分钟，每个envoy最多占用280MB内存，我们增加了proxy容器的内存资源配置，以保存这些时间戳数据。时间戳应该记录在内存中什么具体位置呢？这是通过给每条消息增加唯一x-idx作为其数组下标实现的，每条消息的打点时间戳直接写入指定位置内存，非常高效。
测试结果
envoy延时分布
-
+
我们使用2000QPS进行测试，利用Envoy打点得到了上面的延时分布。从这个分布中，我们发现了一个关键信息：图中1ms ~ 2ms之间的延时分布有隆起现象。高延时部份应该是一些长尾请求造成，应该符合典型的幂律分布，但测试结果表明Envoy造成的延时分布不符合这个特征！
分析优化
经过一些测试之后，我们发现测试过程中CPU资源是Envoy的性能瓶颈，遂猜测Envoy里面有某种任务在长时间运行，来不及转发in-flight的消息，造成这些消息转发不及时。随后，我们对高延时部份的数据在时间分布上进行分析，发现其分布较均匀，因此将目光转移到一些周期性运行的定时任务上。在对Envoy(istio-proxy)代码进行分析后，我们发现istio遥测功能(mixer)在sidecar中会消耗较多的CPU，符合猜测:
-
属性提取中有大量的map操作和字符串拷贝操作
-
+
-
为了节省网络带宽，envoy中对属性上报进行批量处理并压缩
-
+
结合envoy的多线程架构，mixer这种实现方式会造成worker忙于处理上报遥测工作，阻塞业务消息的转发，造成一些请求延时明显增加:
-
+
分析出问题原因之后，我们采用如下的方案进行优化：
- 在Envoy中增加独立的AsyncWorker，专门处理占用CPU但不紧急的逻辑；
@@ -434,11 +435,11 @@ 分析优化
- Worker保存任务上下文，将其提交到队列中暂存，AsyncWorker定时拉取处理；
- 任务队列实现保证lock-free及unbounded特性，防止意外阻塞Worker线程；
-
+
经过优化之后，Envoy内部的延时分布有明显改善：
-
+
总体延时也有一些改善(下图浅蓝色为优化后)：
-
+
通过异步化处理遥测上报操作，我们虽然在延时上获得了明显的优化，但对envoy占用的CPU资源却没有改善，这对大部份应用来说还是不可接受的，随着mixer-less的落地，我们将优化方向转移到降低Envoy CPU消耗，当前的AsyncWorker架构则可以作为通用组件继续保留，与后续优化进行融合，以达到最低的延时。
Istio数据测试对比(已更新，包含1.5遥测)
我们测试了以下几种情况:
@@ -465,26 +466,26 @@ Istio数据测试对比(
吞吐能力
-
+
2vCPU测试下，1.3版本使用mixer实现遥测(1.3-mixer-telemetry)，其最大QPS大约为7000左右；1.5版本使用nullvm的方式(1.5-telemetry-nullvm)则有2000QPS的提升，达到9000左右；关闭telemtry之后(1.3-no-telemetry)，QPS峰值达到13000左右；tke-mesh阻塞优化版的QPS有所下降，只有6000左右，这是因为将上报任务的数据迁移到异步线程中有所消耗。
QPS达到峰值时的CPU资源已成为瓶颈，实际生产环境中我们并不会让系统在如此搞负载下运行。下文的图表中我们只关注5000QPS以下的数据。
延时
P90延时
-
+
P99延时
-
+
使用istio之后，较低QPS负载下延时增加不多，随着QPS的增加延时逐步增大。其中，使用mixer实现的遥测对调用延时影响最明显，即使tke-mesh进行一些优化后，在高负载情况(5000)下，P99也明显增加。istio-1.5使用mixer-less的方案，其延时有明显的改善。
Envoy cpu 消耗
server-side cpu消耗
-
+
client-side cpu 消耗
-
+
可以看出，遥测功能会增加30%左右的CPU消耗，即使1.5版本引入mixer-less的遥测方案，CPU消耗也只在client侧有一些降低。
Envoy memory 消耗
server-side memory
-
+
client-side memory
-
+
Envoy消耗的内存不多，并没有随QPS增加而增加，AsyncWorker方案大约增加了10MB的内存占用，没有太大的影响。
总结
ServiceMesh发展至今，性能问题横在面前，阻碍着其大规模应用。Istio各版本中对性能的一些优化措施没有太好的效果，属于填初期设计的坑：Mixer Cache降低Check对Server的压力，但在实际中可能并有什么效果；遥测上报数据进行delta-Encoding和Compress优化操作，以降低遥测功能产生的网络流量，但带来复杂性的同时又消耗掉可观的CPU；如今推倒重来用Wasm在proxy中实现原来mixer的功能，去掉了mixer-server组件能节约一大笔资源，但数据面性能优化却不是主要目标，其性能并没有质的改变，反而随着Wasm引入而带来的灵活性，大家的目光反而被可扩展性引开。Istio在性能上的缓慢改进的表现，不知道又会损害多少工程师对它的信心，影响其发展速度。
@@ -542,7 +543,7 @@ 总结
©
2017 -
- 2021
+ 2022
diff --git a/post/logic/index.html b/post/logic/index.html
index 7297fa1..4d22979 100644
--- a/post/logic/index.html
+++ b/post/logic/index.html
@@ -215,6 +215,7 @@
\newcommand{\PICK}{\sc{PICK}}
\newcommand{\WITNESS}{\sc{WITNESS}}
\newcommand{\HIDE}{\sc{HIDE}}
+\newcommand{\@w}[1]{\textsf{``{#1}''}}
@@ -448,7 +449,7 @@
- Specifying Systems 笔记2 Liveness & Fairness
+ Specifying Systems 笔记2 Liveness
Prev
@@ -503,7 +504,7 @@
©
2017 -
- 2021
+ 2022
diff --git a/post/page/2/index.html b/post/page/2/index.html
index d3a1f63..0a5735a 100644
--- a/post/page/2/index.html
+++ b/post/page/2/index.html
@@ -187,7 +187,7 @@ 2018
©
2017 -
- 2021
+ 2022
diff --git a/post/specifying-systems-notes-2/index.html b/post/specifying-systems-notes-2/index.html
index eaeac3d..61c9032 100644
--- a/post/specifying-systems-notes-2/index.html
+++ b/post/specifying-systems-notes-2/index.html
@@ -3,7 +3,7 @@
- Specifying Systems 笔记2 Liveness & Fairness - ybyte blog
+ Specifying Systems 笔记2 Liveness - ybyte blog
@@ -16,7 +16,7 @@
-
@@ -46,49 +46,49 @@
-
+
-
+
-
+
-
+
A. Gidenstam, H. Sundell, and P. Tsigas, “Efficient Lock-Free Queues that Mind the Cache,” in 3rd Swedish Workshop on Multi-core Computing (MCC 2010), 2010.
+A. Gidenstam, H. Sundell, and P. Tsigas, “Efficient Lock-Free Queues that Mind the Cache,” 2010.
显示引用列表
[1] A. Gidenstam, H. Sundell, and P. Tsigas, “Efficient Lock-Free Queues that Mind the Cache,” in 3rd Swedish Workshop on Multi-core Computing (MCC 2010), 2010.
+[1] A. Gidenstam, H. Sundell, and P. Tsigas, “Efficient Lock-Free Queues that Mind the Cache,” 2010.
+
+
+
begin_time)，然后接收响应并记录结束时间(end_time)，这样便得到一个请求的延时(end_time - start_time)。当新的发送周期到来时，继续发送下一个请求，记录延时，如此循环…- op: add
path: ${proxy_container_path}/securityContext/privileged
value: true
@@ -402,31 +403,31 @@ 自动化脚本
环境
测试环境使用5台8C16G节点的tke集群。istio-telmetry组件消耗的资源较多，服务端mixs消耗较多，1000QPS大概需要消耗1200m CPU，因此使用两个节点，以满足超过7000QPS的测试压力；pilot等其它控制面组件使用一个节点进行部署； nighthawk和mesh-mocker分别占用一个节点。自动化脚本打包在一个镜像中，每次在控制面组件所在节点运行。
测试中限制了nighthawk、mesh-mocker、envoy都使用2vCPU。同时，考虑到相同资源下，多核机器上worker线程数对并发度有直接影响，最终也会影响延时，因此我们对每个组件的工作线程数也限制为2。这样配置后，在OS调度下，几乎所有组件都是独立运行，不会互相影响，更容易评估使用Istio后envoy产生的影响。
-
+
Envoy打点
Istio数据面带来了明显的延时，把消息在链路中各个阶段的延时统计出来，是进行优化的重要依据。一开始我们思考利用内核态工具如bpftrace进行分析，但请求消息在envoy中进行了多次转发，内核态很难追踪应用层会话，统计时间并不方便，因此我们决定在envoy内部打点记录时间，测试结束后通过离线脚本计算消息在envoy中进行处理的延时。
-
+
client请求server是，每条消息Request依次经过envoy中的3，4，5，6几处，通过readv和writev系统调用读取或发送消息，Response以相反的顺序经过envoy。
我们将Request经过打点位置的时间戳记录为t(*)，将Response经过的时间戳记录为t'(*)，则一条消息在两个sidecar(envoy)中消耗的时间总计为：t(4)-t(3) + t'(3)-t'(4) + t(6)-t(5) + t'(5)-t'(6)。
为了防止打点带来过多的额外损耗，时间戳直接记录在预分配的连续内存（数组）中，如果使用1w QPS测试10分钟，每个envoy最多占用280MB内存，我们增加了proxy容器的内存资源配置，以保存这些时间戳数据。时间戳应该记录在内存中什么具体位置呢？这是通过给每条消息增加唯一x-idx作为其数组下标实现的，每条消息的打点时间戳直接写入指定位置内存，非常高效。
测试结果
envoy延时分布
-
+
我们使用2000QPS进行测试，利用Envoy打点得到了上面的延时分布。从这个分布中，我们发现了一个关键信息：图中1ms ~ 2ms之间的延时分布有隆起现象。高延时部份应该是一些长尾请求造成，应该符合典型的幂律分布，但测试结果表明Envoy造成的延时分布不符合这个特征！
分析优化
经过一些测试之后，我们发现测试过程中CPU资源是Envoy的性能瓶颈，遂猜测Envoy里面有某种任务在长时间运行，来不及转发in-flight的消息，造成这些消息转发不及时。随后，我们对高延时部份的数据在时间分布上进行分析，发现其分布较均匀，因此将目光转移到一些周期性运行的定时任务上。在对Envoy(istio-proxy)代码进行分析后，我们发现istio遥测功能(mixer)在sidecar中会消耗较多的CPU，符合猜测:
-
属性提取中有大量的map操作和字符串拷贝操作
-
+
-
为了节省网络带宽，envoy中对属性上报进行批量处理并压缩
-
+
结合envoy的多线程架构，mixer这种实现方式会造成worker忙于处理上报遥测工作，阻塞业务消息的转发，造成一些请求延时明显增加:
-
+
分析出问题原因之后，我们采用如下的方案进行优化：
- 在Envoy中增加独立的AsyncWorker，专门处理占用CPU但不紧急的逻辑；
@@ -434,11 +435,11 @@ 分析优化
- Worker保存任务上下文，将其提交到队列中暂存，AsyncWorker定时拉取处理；
- 任务队列实现保证lock-free及unbounded特性，防止意外阻塞Worker线程；
-
+
经过优化之后，Envoy内部的延时分布有明显改善：
-
+
总体延时也有一些改善(下图浅蓝色为优化后)：
-
+
通过异步化处理遥测上报操作，我们虽然在延时上获得了明显的优化，但对envoy占用的CPU资源却没有改善，这对大部份应用来说还是不可接受的，随着mixer-less的落地，我们将优化方向转移到降低Envoy CPU消耗，当前的AsyncWorker架构则可以作为通用组件继续保留，与后续优化进行融合，以达到最低的延时。
Istio数据测试对比(已更新，包含1.5遥测)
我们测试了以下几种情况:
@@ -465,26 +466,26 @@ Istio数据测试对比(
吞吐能力
-
+
2vCPU测试下，1.3版本使用mixer实现遥测(1.3-mixer-telemetry)，其最大QPS大约为7000左右；1.5版本使用nullvm的方式(1.5-telemetry-nullvm)则有2000QPS的提升，达到9000左右；关闭telemtry之后(1.3-no-telemetry)，QPS峰值达到13000左右；tke-mesh阻塞优化版的QPS有所下降，只有6000左右，这是因为将上报任务的数据迁移到异步线程中有所消耗。
QPS达到峰值时的CPU资源已成为瓶颈，实际生产环境中我们并不会让系统在如此搞负载下运行。下文的图表中我们只关注5000QPS以下的数据。
延时
P90延时
-
+
P99延时
-
+
使用istio之后，较低QPS负载下延时增加不多，随着QPS的增加延时逐步增大。其中，使用mixer实现的遥测对调用延时影响最明显，即使tke-mesh进行一些优化后，在高负载情况(5000)下，P99也明显增加。istio-1.5使用mixer-less的方案，其延时有明显的改善。
Envoy cpu 消耗
server-side cpu消耗
-
+
client-side cpu 消耗
-
+
可以看出，遥测功能会增加30%左右的CPU消耗，即使1.5版本引入mixer-less的遥测方案，CPU消耗也只在client侧有一些降低。
Envoy memory 消耗
server-side memory
-
+
client-side memory
-
+
Envoy消耗的内存不多，并没有随QPS增加而增加，AsyncWorker方案大约增加了10MB的内存占用，没有太大的影响。
总结
ServiceMesh发展至今，性能问题横在面前，阻碍着其大规模应用。Istio各版本中对性能的一些优化措施没有太好的效果，属于填初期设计的坑：Mixer Cache降低Check对Server的压力，但在实际中可能并有什么效果；遥测上报数据进行delta-Encoding和Compress优化操作，以降低遥测功能产生的网络流量，但带来复杂性的同时又消耗掉可观的CPU；如今推倒重来用Wasm在proxy中实现原来mixer的功能，去掉了mixer-server组件能节约一大笔资源，但数据面性能优化却不是主要目标，其性能并没有质的改变，反而随着Wasm引入而带来的灵活性，大家的目光反而被可扩展性引开。Istio在性能上的缓慢改进的表现，不知道又会损害多少工程师对它的信心，影响其发展速度。
@@ -542,7 +543,7 @@ 总结
©
2017 -
- 2021
+ 2022
diff --git a/post/logic/index.html b/post/logic/index.html
index 7297fa1..4d22979 100644
--- a/post/logic/index.html
+++ b/post/logic/index.html
@@ -215,6 +215,7 @@
\newcommand{\PICK}{\sc{PICK}}
\newcommand{\WITNESS}{\sc{WITNESS}}
\newcommand{\HIDE}{\sc{HIDE}}
+\newcommand{\@w}[1]{\textsf{``{#1}''}}