EagleBear2002 的博客

这里必须根绝一切犹豫，这里任何怯懦都无济于事

发表于 更新于
本文字数： 184 阅读时长 ≈ 1 分钟

摘要

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

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

003 航母下水

国产豪华邮轮交付

阅读全文 »

发表于 更新于
本文字数： 6.3k 阅读时长 ≈ 6 分钟

摘要

本文从行业周期、替换周期和订单交付周期分析了中国船舶行业，重点分析了中国船舶（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

结论前置

阅读全文 »

发表于 更新于
本文字数： 1.9k 阅读时长 ≈ 2 分钟

温竣岩：经济学视角的船舶产业

【十大产业】中国造船业：从寒冬中走来的制造业长子：https://www.bilibili.com/video/BV1RN41157MW/?spm_id_from=333.337.search-card.all.click&vd_source=bd427f91dee5122f5f148ab719220125

该视频分为以下几部分：

上海外高桥船厂：智改数转样板

走进工厂 | 他好像真的想教会我怎么造船：https://www.bilibili.com/video/BV1MP41187Ks/?spm_id_from=333.337.search-card.all.click&vd_source=bd427f91dee5122f5f148ab719220125

阅读全文 »

发表于 更新于 分类于
本文字数： 28k 阅读时长 ≈ 26 分钟

\[ % \def\w{mathsf{w}} % \def\r{mathsf{r}} \def\rd{\textcolor{orange}{\overset{rd}\Longrightarrow}} \def\b{\textcolor{green}{\overset{b}\rightsquigarrow}} \def\rf{\textcolor{green}{\mathsf{rf}}} \def\co{\textcolor{orange}{\mathsf{co}}} \def\fr{\textcolor{purple}{fr}} \def\br{\textcolor{purple}{br}} \def\po{\mathsf{po}} \def\porf{\po\rf} \def\init{\mathsf{init}} \def\next{\mathsf{next}} \def\Event{\mathsf{Event}} % \def\wwrr{\mathsf{w+w+rr}} \def\R{\mathsf{R}} \def\W{\mathsf{W}} \def\Previous{\mathsf{Previous}} \]

摘要

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

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

作者：

阅读全文 »

发表于 更新于 分类于
本文字数： 227 阅读时长 ≈ 1 分钟

摘要

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

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

发表于 更新于 分类于
本文字数： 1.8k 阅读时长 ≈ 2 分钟

摘要

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

关键词：Github Actions，Hexo，Github Pages

为什么要自动部署？

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

阅读全文 »

发表于 更新于 分类于
本文字数： 950 阅读时长 ≈ 1 分钟

摘要

本文梳理了目前主流事务执行历史验证问题的解决方案，对比了各种工具的优劣，尝试提出新的技术路线以改进效率。

验证工具 解决思路 创新点 性能 待改进之处
Cobra1 约束求解 将验证问题建模为 Polygraph 上的约束求解问题 目前已知最高效的 SER 验证工具 未深度整合 SMT
PolySI2 约束求解 将 Polygraph 拓展为 BCpolygraph，同样将 SI 验证问题转化成 BC-polygraph 上的判环问题 PolySI 比 Viper 的性能更为优异，可扩展性也更强，最大规模可以在 40 小时内处理具有百万级事务数量、十亿级键数量的执行历史。 未深度整合 SMT
Viper3 约束求解 问题转化为 polygraph（某种变体）上的判环问题
dbcop4 暴力搜索 dbcop-SER 的性能低于 Cobra，这是因为它会产生大量的无效搜索分支 存在大量无效搜索，内存消耗极大，影响算法可扩展性

  1. Cheng Tan, Changgeng Zhao, Shuai Mu, and Michael Walfish. 2020. COBRA: Making transactional key-value stores verifiably serializable. In OSDI’20.Article 4, 18 pages.↩︎

  2. Kaile Huang, Si Liu, Zhenge Chen, Hengfeng Wei, David Basin, Haixiang Li, and Anqun Pan. Efficient Black-box Checking of Snapshot Isolation in Databases. PVLDB, 16(6): 1264 - 1276, 2023. To appear on PVLDB 2023.↩︎

  3. Jian Zhang, Ye Ji, Shuai Mu, Cheng Tan (2023). Viper: a fast snapshot Isolation Checker. To appear on EuroSys 2023.↩︎

  4. Ranadeep Biswas and Constantin Enea. 2019. On the complexity of checkingtransactional consistency. Proc. ACM Program. Lang. 3, OOPSLA, Article 165 (October 2019), 28 pages.↩︎

发表于 更新于 分类于
本文字数： 18k 阅读时长 ≈ 16 分钟

\[ \def\Var{\mathsf} \def\Val{\mathsf{Val}} \def\OpId{\mathsf{OpId}} \def\Op{\mathsf{Op}} \def\read{\mathsf{read}} \def\write{\mathsf{write}} \def\reads{\mathsf{reads}} \def\writes{\mathsf{writes}} \def\checkSER{\mathsf{checkSER}} \def\size{\mathsf{size}} \def\width{\mathsf{width}} \def\checkSER{\mathsf{checkSER}} \def\Comm{\mathsf{Comm}} \def\SER{\mathsf{SER}} \def\SI{\mathsf{SI}} \def\PC{\mathsf{PC}} \def\CC{\mathsf{CC}} \def\RC{\mathsf{RC}} \def\RA{\mathsf{RA}} \def\Serialization{\mathsf{Serialization}} \def\po{\mathsf{\textcolor{red}{po}}} \def\so{\mathsf{\textcolor{purple}{so}}} \def\wr{\mathsf{\textcolor{green}{wr}}} \def\co{\mathsf{\textcolor{orange}{co}}} \]

摘要

事务通过启用对共享数据的计算来简化并发编程，这些共享数据与其他并发计算隔离并且对故障具有弹性。现代数据库为事务提供了不同的一致性模型，对应于一致性和可用性之间的不同权衡。在这项工作中，我们研究了检查事务数据库的给定执行是否遵循某种一致性模型的问题。我们证明了诸如读提交、读原子和因果一致性之类的一致性模型是多项式时间可检查的，而前缀一致性和快照隔离通常是 NP 完全的。这些结果补充了先前有关可串行性的 NP 完整性结果。此外，在 NP 完全一致性模型的背景下，我们设计了多项式时间的算法，假设输入执行中的某些参数（例如会话数）是固定的。我们在几个生产数据库的背景下评估这些算法的可扩展性。

笔者修改了 DBCop 的部分代码：https://git.nju.edu.cn/EagleBear/dbcop-verifier

INTRODUCTION

阅读全文 »