EagleBear2002 的博客

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

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

（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)

摘要

航空母舰、豪华游轮和 LNG 船因设计建造难度高、附加值高，被合称为造船工业的三大明珠。本文依次举例介绍了三种船型的技术难点和技术突破的重要意义，并分析了中国造船业发展的道路优势和体制优势。

原视频合集链接：飞羽社的个人空间-飞羽社个人主页-哔哩哔哩视频 (bilibili.com)

003 航母下水

国产豪华邮轮交付

摘要

本文从行业周期、替换周期和订单交付周期分析了中国船舶行业，重点分析了中国船舶（600150）股票走势与船舶周期的相关性。本文从公司业务、财务、南北船重组三个角度分析了中国船舶这一企业。笔者在原研报的基础上补充了和环保法规相关的内容。

本研报的视频讲解：https://www.bilibili.com/video/BV14s4y1F7Fh/?spm_id_from=333.999.0.0&vd_source=bd427f91dee5122f5f148ab719220125

有道云笔记原文：https://note.youdao.com/ynoteshare/index.html?id=b181408093cf461258274f9997221073&type=note&_time=1712844592632

结论前置

$$
\def\rd{\textcolor{orange}{\overset{rd}\Longrightarrow}}
\def\b{\textcolor{green}{\overset{b}\rightsquigarrow}}
\def\rf{\mathsf{\textcolor{green}{rf}}}
\def\co{\mathsf{\textcolor{orange}{co}}}
\def\fr{\textcolor{purple}{fr}}
\def\br{\textcolor{purple}{br}}
\def\po{\mathsf{\textcolor{red}{po}}}
\def\porf{\po\rf}
\def\init{\mathsf{init}}
\def\next{\mathsf{next}}
\def\Event{\mathsf{Event}}
\def\R{\mathsf{R}}
\def\W{\mathsf{W}}
\def\Previous{\mathsf{Previous}}
$$

摘要

动态偏序约简（DPOR）通过探索并发程序的所有交错直至某种等价关系（例如 Mazurkiewicz 迹等价）来验证并发程序。这样做涉及空间和时间之间的复杂权衡。现有的 DPOR 算法要么是探索最优的（即仅精确探索每个等价类的交错），但可能使用程序大小的指数内存，要么保持多项式内存消耗，但可能会探索指数级的许多冗余交错。

在本文中，我们表明可以两全其美：在线性内存消耗的情况下探索每个等价类的确切一个交错。我们的算法 TruSt 在 Coq 中形式化，不仅适用于顺序一致性，还适用于满足一些基本假设的任何弱内存模型，包括 TSO、PSO 和 RC11。此外，TruSt 的可并行性令人尴尬：它的不同探索选项没有共享状态，因此可以完全并行探索。因此，TruSt 在内存和/或时间方面优于最先进的技术。

作者：

摘要

顺序一致性是多处理器内存系统中使用最广泛的正确性条件。本文研究了测试共享内存多处理器的问题，以确定它们是否确实提供了顺序一致的内存。它提出了对该问题的首次正式研究，该研究可应用于测试新的内存系统设计和实现、提供运行时容错以及检测并行程序中的错误。

本文提供了一系列结果来测试各种场景下共享内存的执行，将顺序一致性与线性化（另一个众所周知的正确性条件）进行比较。除了顺序一致性之外，线性化对共享内存施加了额外的限制；这些限制被证明在测试此类记忆时很有用。