EagleBear2002 的博客

$$ \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 在内存和/或时间方面优于最先进的技术。

作者：

摘要

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

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

摘要

本文介绍了使用 Github Actions 对 Hexo + Github Pages 博客进行自动部署的方案。考虑到几个月以来 Github 对 HTTPS 协议的限制，本文也列举了笔者的一些失败的实验经历，以供避雷。

关键词：Github Actions，Hexo，Github Pages

为什么要自动部署？

将部署任务从 PC 端转移到云端（例如 Github）的好处包括：

摘要

数据库论文中有许多数学表达式和离散数学概念，本文以蚂蚁老师 2021Spring 的离散数学为大纲，总结了常用的离散数学基础知识，以供参考。

离散数学概论

三个公理系统：逻辑、集合论、抽象代数（群论）。

逻辑