EagleBear2002 的博客

In computing, a memory model describes the interactions of threads through memory and their shared use of the data.

Sequential Consistency (SC) Model [Lamport 1979]

• No muticore processor implements SC
• Compiler optimizations invalidate SC

Weak/Relaxed Memory Models

并发性和正确性

并发对象的正确性往往不容易描述。

如果能将并发执行转化为顺序执行，则只需对该顺序执行进行分析，从而简化了并发对象的分析。

顺序对象

每个对象都有一个状态，通常由一组字段（field）给出。队列示例：项目序列。

Using Locks

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

public class Counter {
	private long value;
	private Lock lock;

	public long getAndIncrement() {
		lock.lock(); // acquire lock
		try { // critical section
			int temp = value;
			value = value + 1;
		} finally {
			lock.unlock(); // release lock, no matter what
		}
		return temp;
	}
}

两个 Liveness

避免死锁 Deadlock-Free：如果某个线程调用 lock()，并且从不返回，那么其他线程必须无限次地完成 lock() 和 unlock() 调用。整个系统都会取得进展，即使某个线程饿死。

避免饿死 Starvation-Free：如果某个线程调用 lock()，它最终会返回，各个线程取得进展。

Amdahl’s Law

$$ Speedup = \frac{\text{1-thread execution time}}{\text{n-thread execution time}} \\ = \frac{1}{1 - p + \frac{p}{n}} $$

其中 p 是并发执行的代码在所有代码中的比例。

Safety & Linvness 安全性和活跃性

liveness 在中文版教材中被翻译为演进条件。

为贯彻落实党的二十大作出的战略部署，二十届中央委员会第三次全体会议研究了进一步全面深化改革、推进中国式现代化问题，作出如下决定。

进一步全面深化改革、推进中国式现代化的重大意义和总体要求

（1）进一步全面深化改革的重要性和必要性。改革开放是党和人民事业大踏步赶上时代的重要法宝。党的十一届三中全会是划时代的，开启了改革开放和社会主义现代化建设新时期。党的十八届三中全会也是划时代的，开启了新时代全面深化改革、系统整体设计推进改革新征程，开创了我国改革开放全新局面。

以习近平同志为核心的党中央团结带领全党全军全国各族人民，以伟大的历史主动、巨大的政治勇气、强烈的责任担当，冲破思想观念束缚，突破利益固化藩篱，敢于突进深水区，敢于啃硬骨头，敢于涉险滩，坚决破除各方面体制机制弊端，实现改革由局部探索、破冰突围到系统集成、全面深化的转变，各领域基础性制度框架基本建立，许多领域实现历史性变革、系统性重塑、整体性重构，总体完成党的十八届三中全会确定的改革任务，实现到党成立一百周年时各方面制度更加成熟更加定型取得明显成效的目标，为全面建成小康社会、实现党的第一个百年奋斗目标提供有力制度保障，推动我国迈上全面建设社会主义现代化国家新征程。

（2024 年 7 月 18 日中国共产党第二十届中央委员会第三次全体会议通过）

中国共产党第二十届中央委员会第三次全体会议，于 2024 年 7 月 15 日至 18 日在北京举行。

出席这次全会的有，中央委员 199 人，候补中央委员 165 人。中央纪律检查委员会常务委员会委员和有关方面负责同志列席会议。党的二十大代表中部分基层同志和专家学者也列席了会议。

全会由中央政治局主持。中央委员会总书记习近平作了重要讲话。

全会听取和讨论了习近平受中央政治局委托所作的工作报告，审议通过了《中共中央关于进一步全面深化改革、推进中国式现代化的决定》。习近平就《决定（讨论稿）》向全会作了说明。

$$ \def\po{\mathsf{\textcolor{red}{po}}} \def\AR{\mathsf{\textcolor{brown}{AR}}} \def\VIS{\mathsf{\textcolor{orange}{VIS}}} \def\Obj{\mathsf{Obj}} \def\Op{\mathsf{Op}} \def\Hist{\mathsf{Hist}} \def\Event{\mathsf{Event}} \def\REvent{\mathsf{REvent}} \def\WEvent{\mathsf{WEvent}} \def\HEvent{\mathsf{HEvent}} \def\EventId{\mathsf{EventId}} \def\read{\mathtt{read}} \def\write{\mathtt{write}} \def\H{\mathcal{H}} \def\A{\mathcal{A}} $$

摘要

现代分布式系统通常依赖于数据库，这些数据库通过仅提供关于分布式事务处理一致性的弱保证来实现可扩展性。与此类数据库交互的程序的语义取决于其一致性模型，该模型定义了这些保证。不幸的是，一致性模型通常是非正式的或使用不同的形式主义，通常与数据库内部相关。为了解决这个问题，我们提出了一个框架，用于统一和声明性地指定各种事务一致性模型。

我们的规范以弱内存模型的形式给出，使用事件和关系结构。这些规范特别简洁，因为它们利用了许多一致性模型保证的原子可见性属性：事务的所有更新或所有更新都对另一个事务可见。这允许规范从事务内部的单个事件中抽象出来。我们通过指定几个现有的一致性模型来说明我们框架的使用。为了验证我们的规范，我们证明它们等同于替代操作规范，这些规范是更接近实际实现的算法。我们的工作为开发弱一致性大规模数据库中出现的新形式并发的元理论提供了严格的基础。

作者：

$$ \def\wr{\mathsf{\textcolor{teal}{wr}}} \def\ww{\mathsf{\textcolor{red}{ww}}} $$

摘要

分布式数据库系统出现了支持多协调器和多副本存储的新架构，这给事务调度的正确性带来了新的挑战，包括缺少中心协调器带来的新数据异常以及多副本机制带来的读取数据一致性等问题。基于事务隔离级别和分布式系统一致性协议的定义，为多协调器多副本分布式数据库的事务多级一致性构建了一个混合依赖图模型。该形式化模型为事务的正确调度提供具有鲁棒性的评价标准，可以方便地对数据库事务调度情况进行动态或静态分析检验.

作者：数据工程与知识工程教育部重点实验室(中国人民大学)、中国人民大学 信息学院 水治禹、卢卫、赵展浩、何粤阳、张孝、杜小勇

基于环的数据异常与隔离级别定义

摘要

铅酸蓄电池电动车使用经验有二：电量表无法正确显示剩余电量；匀速行驶可以增加电池续航里程。本文从电化学角度和电路角度分析了铅酸蓄电池工作原理，解释了这两个工程现象。

铅酸蓄电池电化学反应

铅酸蓄电池正极材料为 $\ce{PbO2}$，负极材料为 $\ce{Pb}$，电解质为 $\ce{H2SO4}$。

摘要

本文

原文链接：各种船型定义（带你入门比较好的资料） (qq.com)