EagleBear2002 的博客

CONCUR’18 Anode[^Kartik]

SQL 编码为 FOL，基础理论，无代码；

SIGMOD’22 WeTune[^WeTune]

SIGMOD2022 WeTune，王肇国等。

• Databend-【论文分享｜ SIGMOD’22】WeTune 自动发现和验证重写规则：https://zhuanlan.zhihu.com/p/630112740
• Gauss 松鼠会-WeTune：一种可以自动合成重写规则的规则生成器：https://www.zhihu.com/zvideo/1530486978957414400

$$
\def\vis{\mathsf{\textcolor{orange}{vis}}}
\def\ar{\mathsf{\textcolor{pink}{ar}}}
\def\RW{\mathsf{RW}}
\def\WW{\mathsf{\textcolor{red}{WW}}}
\def\WR{\mathsf{\textcolor{blue}{WR}}}
\def\visa{\xrightarrow{\vis}}
\def\ara{\xrightarrow{\ar}}
\def\RWa{\xrightarrow{\RW}}
\def\WWa{\xrightarrow{\WW}}
\def\WRa{\xrightarrow{\WR}}
\def\wri{\mathsf{wri}}
\def\Stmts{\mathtt{Stmts}}
\def\IF{\mathtt{IF}}
\def\true{\mathsf{true}}
\def\AccID{\mathtt{AccID}}
\def\ID{\mathtt{ID}}
\def\bal{\mathtt{bal}}
\def\Amount{\mathtt{Amount}}
\def\Alive{\mathtt{Alive}}
\def\Fields{\mathtt{Fields}}
\def\T{\mathcal{T}}
\def\R{\mathcal{R}}
\def\D{\mathcal{D}}
\def\V{\mathcal{V}}
\def\bbT{\mathbb{T}}
\def\bbV{\mathbb{V}}
\def\bbZ{\mathbb{Z}}
\def\B{\mathbb{B}}
\def\v{\mathtt{v}}
\def\f{\mathtt{f}}
\def\FOREACH{\texttt{ FOREACH}}
\def\IN{\texttt{ IN}}
\def\DO{\texttt{ DO}}
\def\END{\texttt{ END}}
\def\NULL{\texttt{ NULL}}
\def\Vars{\texttt{ Vars}}
\def\LVar{\texttt{ LVar}}
$$

摘要

尽管近年来开发了许多弱一致性机制来提高分布式复制系统的性能并确保可用性，但确保在此类系统上运行的事务应用程序的正确性仍然是一个困难而重要的问题。可串行化是事务性程序的一个众所周知的正确性标准； 然而，了解应用程序在弱一致性环境中执行时是否可序列化仍然是一项具有挑战性的工作。在这项工作中，我们结合了基于依赖图的可串行化特征，并利用抽象执行框架来开发一种全自动方法，用于在任何弱一致性模型下静态查找有界可串行化违规。我们将可序列化问题简化为一阶逻辑（FOL）中公式的可满足性问题，这使我们能够利用现有 SMT 求解器的功能。我们提供了从用 SQL 编写的程序（允许循环和条件）自动构造 FOL 编码的规则，并将一致性规范表示为 FOL 公式。除了检测有界可串行性违规之外，我们还提供了两种正交方案，通过提供充分的条件（同样以 FOL 公式的形式）来推理无界执行，其可满足性意味着在任何任意执行中都不存在异常。我们已将所提出的技术应用于 TPC-C（一个具有复杂应用程序逻辑的现实数据库程序），并且能够发现并行快照隔离（PSI）下的异常，并验证快照隔离（SI）下无限执行的可串行性，两个远弱于可串行化的一致性机制。

Nagar 与 Jagannathan 在本文中使用一阶谓词逻辑公式对客户程序以及事务一致性模型进行精确建模，利用 SAT/SMT 自动推导出违反该一致性的执行历史的结构，并在客户程序可能产生的所有执行历史中搜索该结构。

本文的工作是基于分布式数据一致性。

TODO：SQL 中的循环是否是必须的？

本文主要内容来自 SpriCoder 的博客，更换了更清晰的图片并根据新的课程设计做了补充和修正。

【2014】自主团队

【2013】【2015A】【2016】软件开发是知识工作

软件开发是一项既复杂又富有创造性的知识工作

软件开发——智力劳动：

摘要

本文梳理了数据库事务的发展史。在 SQL 标准规定的 SER、RR、RC 和 RU 之外，重点介绍了 SI 隔离级别。本文还介绍了提高事务隔离级别的几种方式，并展望了未来可能出现的高效 SER 的实现方式。本文是 数据库事务发展史+SSI 隔离级别原理 课程笔记。

1992 年：ANSI SQL92 事务隔离级别

Dirty Read、Fuzzy Read 和 Phantom 分别表示脏读、不可重复读、幻读三种异象（phenomenon）。

摘要

本文介绍了基于 NJU-Table 协同表格的新生车辆入校审批系统的需求明细、视图展示和部分设计细节，并记录了系统上线运行后得到的反馈。在新生学院七个书院十余位老师的共同支持下，该系统在开学两天内顺利调度一千二百余辆私家车错峰入校，展示了后疫情时代信息化行政的强大潜力。该系统的开发涉及到 NJU-Table 向非专业开发者提供的绝大多数功能，为学习使用 NJU-Table 提供了良好范例。

需求明细

• [x] 新生扫描二维码或点击链接，在移动端或 PC 端通过表单提交姓名、学号、所在书院、车牌号，选择停泊时间
• [x] 新生只能在书院规定的报道时间内选择停泊时间
• [x] 仅书院负责审核的辅导员可在相应视图（如“健雄书院审核视图”）对本书院的提交完成审核
• [x] 要求填写者承诺在填写的停泊时间结束前离开学校
• [x] 申请被审核后新生可在系统中收到通知（目前无法使用微信、邮件等第三方通知）
• [x] 新生可查看已提交的申请的审核情况
• [x] 可以自动检测一人多填，保证每个人最多只能填写一个有效表单
• [ ] 系统自动限制每个时间段的停泊数量

系统视图展示

下载

Github 上的 clash 官方仓库已经删库跑路，本文介绍的是一个目前可行的解决方案。

在 https://github.com/doreamon-design/clash/releases 下载与自己系统架构符合的安装包。一般选择 [clash_2.0.24_linux_amd64.tar.gz](https://github.com/doreamon-design/clash/releases/download/v2.0.24/clash_2.0.24_linux_amd64.tar.gz)。

安装

1
2
3
4

gzip -d clash_2.0.24_linux_amd64.tar.gz # 在安装包所在路径解压安装包
chmod +x clash_2.0.24_linux_amd64.tar.gz # 给解压后的文件赋予执行权限
mv clash_2.0.24_linux_amd64 /usr/local/bin/clash # 移动文件位置
clash -v # 查看是否成功安装

哪些人的理性会受挫？

进电影院前的我：

夫未战而庙算胜者，得算多也，未战而庙算不胜者，得算少也。多算胜，少算不胜，而况于无算乎！吾以此观之，胜负见矣。（《孙子兵法》）故曰：善战者无赫赫之功（曹操）。

看完电影后的我：

人算不如天算：行人是，知天命，可以无悔矣。

题面

请在南京大学校园网环境下访问：🫡Jo 娜贝尔 (Bye-JonaBell.c) (cpl.icu)

题解

50 分算法

课上讲过的作业题 JoJo 谜题 (josephus.c) (cpl.icu)。

摘要

本文是 2023 年南京大学软件学院推免经验分享内容。

南软学硕基本信息

登录南京大学研招网查看当年权威信息：https://yzb.nju.edu.cn/main.htm

原文链接：通俗易懂 强一致性、弱一致性、最终一致性、读写一致性、单调读、因果一致性 的区别与联系 - 知乎 (zhihu.com)

提到分布式架构就一定绕不开“一致性”问题，而“一致性”其实又包含了数据一致性和事务一致性两种情况，本文主要讨论数据一致性（事务一致性指 ACID）。

复制是导致出现数据一致性问题的唯一原因。

如果只用一台数据库来处理所有的写入和读取请求，就一定不存在数据一致性的问题。 但在中大型项目中，我们却经常需要将一份数据存储在超过一台数据库中（即复制），原因有三：

1. 即使一部分数据库出现故障，系统也能正常工作（高可用）
2. 使数据与用户在地理上接近（降低延迟）
3. 扩展可以处理读请求的机器数量（可扩展性、提高读取吞吐量）