feat: deploy github page

zh-cn/assets/index-d11993a8.js → zh-cn/assets/index-0cf6ee95.js

@@ -1,4 +1,4 @@
-const e="/zh-cn/assets/cover-c17c52cc.png",s="/zh-cn/assets/image1-0dff4570.png",c="/zh-cn/assets/image2-e09cfdc8.png",o="/zh-cn/assets/image3-2b589463.png",a="/zh-cn/assets/image4-5841c9d6.png",p="/zh-cn/assets/image5-92344f1d.png",d="/zh-cn/assets/image6-b429f851.png",r="/zh-cn/assets/image7-97920b5a.png",i="/zh-cn/assets/image8-ecf5c6f3.png",t="/zh-cn/assets/image9-f47bad66.png",n="/zh-cn/assets/image10-b50adc27.png",l="/zh-cn/assets/image11-99ec2a51.png",m=[e,s,c,o,a,p,d,r,i,t,n,l],h={label:"从数学角度思考程序与验证正确性",description:"本文旨在为没有接触过形式化方法的读者提供一种新的视角看待计算机系统与算法，而非形式化方法或 TLA+ 教程。因此本文的重点是如何从数学角度思考程序，不会使用大篇幅讲解 TLA+ 的语法。",cover:"./cover.png",location:"中国香港",author:["田野"],tags:["Xline"],date:"2023-03-02",title:"Thinking about programs mathematically and verifying correctness"},g=[{label:"我们该如何写出正确的程序？",level:2},{label:"程序中会有什么样错误？",level:3},{label:"经验",level:3},{label:"形式化方法",level:3},{label:"TLA+",level:2},{label:"简单的例子",level:3},{label:"Two-Phase Commit",level:2},{label:"总结",level:2},{label:"我们的项目：Xline",level:2}],T=`<p><img src="${e}" alt="封面"></p>
+const e="/zh-cn/assets/cover-c17c52cc.png",s="/zh-cn/assets/image1-0dff4570.png",c="/zh-cn/assets/image2-e09cfdc8.png",o="/zh-cn/assets/image3-2b589463.png",a="/zh-cn/assets/image4-5841c9d6.png",p="/zh-cn/assets/image5-92344f1d.png",d="/zh-cn/assets/image6-b429f851.png",r="/zh-cn/assets/image7-97920b5a.png",t="/zh-cn/assets/image8-ecf5c6f3.png",i="/zh-cn/assets/image9-f47bad66.png",n="/zh-cn/assets/image10-b50adc27.png",l="/zh-cn/assets/image11-99ec2a51.png",m=[e,s,c,o,a,p,d,r,t,i,n,l],h={label:"从数学角度思考程序与验证正确性",description:"本文旨在为没有接触过形式化方法的读者提供一种新的视角看待计算机系统与算法，而非形式化方法或 TLA+ 教程。因此本文的重点是如何从数学角度思考程序，不会使用大篇幅讲解 TLA+ 的语法。",cover:"./cover.png",location:"中国香港",author:["田野"],tags:["Xline"],date:"2023-03-02",title:"Thinking about programs mathematically and verifying correctness"},g=[{label:"我们该如何写出正确的程序？",level:2},{label:"程序中会有什么样错误？",level:3},{label:"经验",level:3},{label:"形式化方法",level:3},{label:"TLA+",level:2},{label:"简单的例子",level:3},{label:"Two-Phase Commit",level:2},{label:"总结",level:2},{label:"我们的项目：Xline",level:2}],A=`<p><img src="${e}" alt="封面"></p>
 <p>本文旨在为没有接触过形式化方法的读者提供一种新的视角看待计算机系统与算法，而非形式化方法或 TLA+ 教程。因此本文的重点是如何从数学角度思考程序，不会使用大篇幅讲解 TLA+ 的语法。</p>
 <h2 id="我们该如何写出正确的程序？">我们该如何写出正确的程序？</h2>
 <p>程序设计的目标永远是写出正确的程序。随着时间的推移，我们的程序越来越复杂，其中可能存在的错误也越来越多。想要写出正确的程序，首先应该了解程序中可能出现的错误有哪些。</p>
@@ -112,9 +112,9 @@ Next 用于定义状态转换关系。</p>
 <li><code>UNCHANGED ⟨rmState, tmState, msgs⟩</code> 表示这个动作不会改变 <code>rmState</code>、<code>tmState</code>、<code>msgs</code> 这三个变量的值。在 TLA+ 中，每一个变量的值是否改变都需要显式地声明。</li>
 </ul>
 <p>当 <code>TM</code> 的状态为 <code>init</code>，且在消息池中存在来自 <code>r</code> 的 <code>Prepared</code> 消息，<code>tmPrepared</code> 在下一个状态的值会是 <code>tmPrepared</code> 和 <code>{r}</code> 的并集。</p>
-<p><img src="${i}" alt="图片"></p>
-<p>上面的两个动作分别是 Transaction Manager 进行 Commit 与 Abort。</p>
 <p><img src="${t}" alt="图片"></p>
+<p>上面的两个动作分别是 Transaction Manager 进行 Commit 与 Abort。</p>
+<p><img src="${i}" alt="图片"></p>
 <p>上述 4 个 Resource Manager 动作分别是 Resource Manager 选择 Prepare 与 Abort，以及处理由 Transaction Manager 决定的 Commit 与 Abort。</p>
 <p>其中，存在语法如 <code>rmState' = [rmState except ![r] = "prepared"]</code>，意为"在下一个状态中，<code>rmState[r]</code> 的值变为 <code>prepared</code>，其它部分不变"。</p>
 <p>如果我们用形如 <code>rmState[r]' = "prepared"</code> 的形式来表示，我们并没有显式地说明 <code>rmState</code> 的其它部分在下一个状态的值，因此是不正确的。</p>
@@ -149,4 +149,4 @@ Next 用于定义状态转换关系。</p>
 <h2 id="我们的项目：xline">我们的项目：Xline</h2>
 <p>TLA+被广泛用于分布式系统算法的研究和开发中。在我们的项目 Xline 中，TLA+被用来在设计阶段验证共识算法的正确性。</p>
 <p>Xline 是一个用于元数据管理的分布式 KV 存储。我们在 Xline 中使用 CURP 协议（<a href="https://www.usenix.org/system/files/nsdi19-park.pdf)%E7%9A%84%E4%BF%AE%E6%94%B9%E7%89%88%E4%BD%9C%E4%B8%BA%E5%85%B1%E8%AF%86%E5%8D%8F%E8%AE%AE%EF%BC%8CTLA+%E5%B0%86%E8%A2%AB%E7%94%A8%E4%BA%8E%E5%85%B6%E6%AD%A3%E7%A1%AE%E6%80%A7%E9%AA%8C%E8%AF%81%E4%B8%AD%E3%80%82">https://www.usenix.org/system/files/nsdi19-park.pdf)的修改版作为共识协议，TLA+将被用于其正确性验证中。</a></p>
-<p>如果你想了解更多关于 Xline 的信息，请参考我们的 Github：<a href="https://github.com/datenlord/Xline">https://github.com/datenlord/Xline</a></p>`;export{m as assetURLs,T as default,h as metadata,g as toc};
+<p>如果你想了解更多关于 Xline 的信息，请参考我们的 Github：<a href="https://github.com/datenlord/Xline">https://github.com/datenlord/Xline</a></p>`;export{m as assetURLs,A as default,h as metadata,g as toc};

zh-cn/assets/index-192ae9c1.js → zh-cn/assets/index-102c2147.js

@@ -1,4 +1,4 @@
-const s="/zh-cn/assets/cover-48216986.png",t="/zh-cn/assets/image1-02771bf0.jpg",n="/zh-cn/assets/image1-f46bfcc6.jpg",r=[s,t,n],o={label:"当RDMA遇到Rust",description:"2022年8月5日-6日，一年一度的中国开源基础设施活动日（OpenInfra Days China）即将在线上举行。本次会议没有限定一个统一的主题，主要聚焦云计算基础设施、云原生技术与应用实践、开源治理、5G、算力网络与边缘计算五大主题方向。",cover:"./cover.png",location:"新加坡",date:"2022-08-04",title:"When RDMA meets Rust"},p=[],a=`<p><img src="${s}" alt="封面"></p>
+const s="/zh-cn/assets/cover-48216986.png",t="/zh-cn/assets/image1-02771bf0.jpg",n="/zh-cn/assets/image1-f46bfcc6.jpg",o=[s,t,n],p={label:"当RDMA遇到Rust",description:"2022年8月5日-6日，一年一度的中国开源基础设施活动日（OpenInfra Days China）即将在线上举行。本次会议没有限定一个统一的主题，主要聚焦云计算基础设施、云原生技术与应用实践、开源治理、5G、算力网络与边缘计算五大主题方向。",cover:"./cover.png",location:"新加坡",date:"2022-08-04",title:"When RDMA meets Rust"},r=[],g=`<p><img src="${s}" alt="封面"></p>
 <p>2022 年 8 月 5 日-6 日，**一年一度的中国开源基础设施活动日（OpenInfra Days China）**即将在线上举行。本次会议没有限定一个统一的主题，主要聚焦云计算基础设施、云原生技术与应用实践、开源治理、5G、算力网络与边缘计算五大主题方向。</p>
 <p><strong>云计算基础设施分论坛</strong>主要聚焦云计算基础设施领域的前沿技术和优秀实践，围绕多硬件架构和多操作系统支持、人工智能技术应用、网络与存储，数据处理 DPU 及其他加速硬件、硬件自动化和智能运维等方面展开技术分享和探讨。达坦科技联合创始人施继成将在这一分论坛做题为<strong>当 RDMA 遇到 Rust</strong> 的专题分享。</p>
 <p><img src="${t}" alt="图片"></p>
@@ -10,4 +10,4 @@ const s="/zh-cn/assets/cover-48216986.png",t="/zh-cn/assets/image1-02771bf0.jpg"
 <h4>参会方式</h4>
 <p>想要了解更多达坦科技为什么选择 Rust 做 RDMA 库，以及开发设计背后的理念、逻辑、和实践经验，欢迎扫描海报二维码，免费注册报名。</p>
 <p>有意加入 <strong>Rust 前沿交流讨论群</strong>，请添加小助手微信：</p>
-<p><img src="${n}" alt="图片"></p>`;export{r as assetURLs,a as default,o as metadata,p as toc};
+<p><img src="${n}" alt="图片"></p>`;export{o as assetURLs,g as default,p as metadata,r as toc};

zh-cn/assets/index-a806d623.js → zh-cn/assets/index-12e593c9.js

@@ -1,4 +1,4 @@
-const t="/zh-cn/assets/cover-39643179.png",e="/zh-cn/assets/image1-a93ba076.jpg",s="/zh-cn/assets/image2-4624885a.gif",p="/zh-cn/assets/image3-ea54df7e.jpg",a=[t,e,s,p],c={label:"直播预告 | RDMA软件接口高层封装",description:"RDMA 作为高速通信协议被数据中心广泛使用，但是因为底层接口设计得过于繁复，对使用者造成了很大的不便，因此我们使用 Rust 语言对 RDMA 进行了一层高层封装。这次分享将介绍这层封装的做法和原理。",cover:"./cover.png",location:"香港",date:"2022-05-17",title:"RDMA Software Interface High Level Package"},l=[{label:"嘉宾介绍",level:2},{label:"讨论内容",level:2},{label:"观看方式",level:2},{label:"特别鸣谢",level:2}],n=`<h2 id="嘉宾介绍">嘉宾介绍</h2>
+const p="/zh-cn/assets/cover-39643179.png",e="/zh-cn/assets/image1-a93ba076.jpg",s="/zh-cn/assets/image2-4624885a.gif",a="/zh-cn/assets/image3-ea54df7e.jpg",t=[p,e,s,a],c={label:"直播预告 | RDMA软件接口高层封装",description:"RDMA 作为高速通信协议被数据中心广泛使用，但是因为底层接口设计得过于繁复，对使用者造成了很大的不便，因此我们使用 Rust 语言对 RDMA 进行了一层高层封装。这次分享将介绍这层封装的做法和原理。",cover:"./cover.png",location:"香港",date:"2022-05-17",title:"RDMA Software Interface High Level Package"},l=[{label:"嘉宾介绍",level:2},{label:"讨论内容",level:2},{label:"观看方式",level:2},{label:"特别鸣谢",level:2}],n=`<h2 id="嘉宾介绍">嘉宾介绍</h2>
 <p>施继成</p>
 <p>达坦科技联合创始人兼 CTO，复旦大学软件工程本硕，师从华为基础软件首席科学家、鸿蒙实验室主任陈海波教授。擅长操作系统内核开发、分布式系统、嵌入式系统，对分布式数据一致性有钻深的研究，发表多篇操作系统内核相关论文，累计数百次引用。毕业后曾在谷歌中国、微软亚太和阿里巴巴等公司从事分布式计算和存储等相关工作。入选 2022 年度 6 氪 S 级创业者名册，荣获中国“企业工具与底层软件”领域 “36 位 36 岁以下创业者“称号。</p>
 <h2 id="讨论内容">讨论内容</h2>
@@ -16,5 +16,5 @@ const t="/zh-cn/assets/cover-39643179.png",e="/zh-cn/assets/image1-a93ba076.jpg"
 <p><img src="${s}" alt="图片"></p>
 <p><strong>转发本文，文末留言提问、加群提问、或者现场提问，我们将赠送 1 本书，数量有限，送完为止。</strong></p>
 <p>↓ 扫码加入本次直播交流群；</p>
-<p><img src="${p}" alt="图片"></p>
-<p>咨询的小伙伴，可添加小月@阅码场的微信 <strong>Linuxer2016</strong> 咨询</p>`;export{a as assetURLs,n as default,c as metadata,l as toc};
+<p><img src="${a}" alt="图片"></p>
+<p>咨询的小伙伴，可添加小月@阅码场的微信 <strong>Linuxer2016</strong> 咨询</p>`;export{t as assetURLs,n as default,c as metadata,l as toc};