技术,生活,随看 \随转
https://thebarentsobserver.com/en/security/2020/08/rosatom-releases-previously-classified-documentary-video-50-mt-novaya-zemlya-test
The Independent Barents Observer
Rosatom releases previously classified documentary video of Tsar
Photos and short video clips have previously been available, but this unseen 40 minutes declassified footage of the Soviet Union’s monster nuclear bomb give a whole new insight into what happened on
Rust 核心团队成员 RalfJung 的PhD 毕业论文
Ralf 说：
「
完成了！ 我的论文终于完成了。 因此，如果您一直想深入了解我对Rust的研究（以及更多），可以阅读我的论文。 它有近300页，应该会让您忙一阵子。 ;）
这也意味着，经过六年多的学习，我成为博士生的时间已经结束了。实际上，我当了十多年的学生了，是时候结束了。 真是奇怪的感觉。
接下来肯定会继续做很多 Rusty 的事情，从事更多技术性的工作，研究迄今为止还没有研究过的东西。
」
Blessing！
https://www.ralfj.de/blog/2020/09/03/phd.html
论文简介：
论文提出了两个项目，这些项目为Rust的正式基础奠定了基础，使我们能够更好地理解和发展这一重要语言：RustBelt和Stacked Borrows。
RustBelt是Rust类型系统的形式化模型，并具有健全的内存和线程安全性证明。 该模型旨在验证Rust标准库中许多复杂API的安全性，尽管这些API的实现使用了Unsafe的语言功能。
Stacked Borrows 是对Rust规范的建议扩展，它使编译器可以使用Rust类型的强别名信息来更好地分析和优化其正在编译的代码。 不仅可以正式评估该规范的适当性，还可以在实现了Stacked Borrows语义的Rust的Miri解释器的实际版本中运行真实的Rust代码。
RustBelt建立在Iris（语言无关的框架）之上，该框架在Coq proof assistant中实现，用于构建更高阶的并发分离（ higher-order concurrent separation）逻辑。 本文首先介绍了Iris，并解释了Iris 如何从一些简单的成分中衍生出复杂的高级推理原理。 在RustBelt中，该技术被关键地用来引入生命周期逻辑，该逻辑提供了新颖的借用分离逻辑说明，这是Rust类型系统的关键突出特性。
论文下载地址： https://people.mpi-sws.org/~jung/thesis.html
Ralf 说：
「
完成了！ 我的论文终于完成了。 因此，如果您一直想深入了解我对Rust的研究（以及更多），可以阅读我的论文。 它有近300页，应该会让您忙一阵子。 ;）
这也意味着，经过六年多的学习，我成为博士生的时间已经结束了。实际上，我当了十多年的学生了，是时候结束了。 真是奇怪的感觉。
接下来肯定会继续做很多 Rusty 的事情，从事更多技术性的工作，研究迄今为止还没有研究过的东西。
」
Blessing！
https://www.ralfj.de/blog/2020/09/03/phd.html
论文简介：
论文提出了两个项目，这些项目为Rust的正式基础奠定了基础，使我们能够更好地理解和发展这一重要语言：RustBelt和Stacked Borrows。
RustBelt是Rust类型系统的形式化模型，并具有健全的内存和线程安全性证明。 该模型旨在验证Rust标准库中许多复杂API的安全性，尽管这些API的实现使用了Unsafe的语言功能。
Stacked Borrows 是对Rust规范的建议扩展，它使编译器可以使用Rust类型的强别名信息来更好地分析和优化其正在编译的代码。 不仅可以正式评估该规范的适当性，还可以在实现了Stacked Borrows语义的Rust的Miri解释器的实际版本中运行真实的Rust代码。
RustBelt建立在Iris（语言无关的框架）之上，该框架在Coq proof assistant中实现，用于构建更高阶的并发分离（ higher-order concurrent separation）逻辑。 本文首先介绍了Iris，并解释了Iris 如何从一些简单的成分中衍生出复杂的高级推理原理。 在RustBelt中，该技术被关键地用来引入生命周期逻辑，该逻辑提供了新颖的借用分离逻辑说明，这是Rust类型系统的关键突出特性。
论文下载地址： https://people.mpi-sws.org/~jung/thesis.html
中国孩子在日本开刀住院的帐单：16万人民币只需自掏740元饭钱 - 南木香的文章 - 知乎
https://zhuanlan.zhihu.com/p/212770012
https://zhuanlan.zhihu.com/p/212770012
亚马逊官宣：全面推出 Bottlerocket – 专为运行容器而打造的基于 Linux 的全新开源操作系统
发布于: Aug 31, 2020
今天，Amazon Web Services (AWS) 宣布全面推出 Bottlerocket （纯 Rust 实现），这是一种专为运行容器而打造的基于 Linux 的全新开源操作系统 (OS)。Bottlerocket 仅包括运行容器所需的软件，并且附带事务更新机制。这些属性使客户能够使用容器协调器以最小的中断来管理操作系统更新，从而提高容器化应用程序的安全性并降低运营成本。AWS 提供的 Bottlerocket 映像适用于 Amazon EKS (GA) 和 Amazon ECS（预览版）。Bottlerocket 是作为 GitHub 上的开源项目开发的。
如今，大多数容器都在通用操作系统上运行，而这些操作系统旨在支持以各种格式封装的应用程序。此类操作系统需要数百个软件包，需要频繁的安全和维护更新，即使只有少数软件包用于运行容器化应用程序。Bottlerocket 专注于安全性，并通过仅包含托管容器必需的软件来减少遭受攻击的机会。它附带安全增强型 Linux (SELinux)，以强制模式增加隔离，并使用 Device Mapper 的一个 Linux 内核功能 verity 目标 (dm-verity) 来帮助防止基于 rootkit 的攻击。除了这些安全增强功能之外，还以原子方式对 Bottlerocket 更新进行了应用和回滚，以进一步简化更新管理。
https://github.com/bottlerocket-os/bottlerocket
https://amazonaws-china.com/cn/about-aws/whats-new/2020/08/announcing-general-availability-of-bottlerocket/
发布于: Aug 31, 2020
今天，Amazon Web Services (AWS) 宣布全面推出 Bottlerocket （纯 Rust 实现），这是一种专为运行容器而打造的基于 Linux 的全新开源操作系统 (OS)。Bottlerocket 仅包括运行容器所需的软件，并且附带事务更新机制。这些属性使客户能够使用容器协调器以最小的中断来管理操作系统更新，从而提高容器化应用程序的安全性并降低运营成本。AWS 提供的 Bottlerocket 映像适用于 Amazon EKS (GA) 和 Amazon ECS（预览版）。Bottlerocket 是作为 GitHub 上的开源项目开发的。
如今，大多数容器都在通用操作系统上运行，而这些操作系统旨在支持以各种格式封装的应用程序。此类操作系统需要数百个软件包，需要频繁的安全和维护更新，即使只有少数软件包用于运行容器化应用程序。Bottlerocket 专注于安全性，并通过仅包含托管容器必需的软件来减少遭受攻击的机会。它附带安全增强型 Linux (SELinux)，以强制模式增加隔离，并使用 Device Mapper 的一个 Linux 内核功能 verity 目标 (dm-verity) 来帮助防止基于 rootkit 的攻击。除了这些安全增强功能之外，还以原子方式对 Bottlerocket 更新进行了应用和回滚，以进一步简化更新管理。
https://github.com/bottlerocket-os/bottlerocket
https://amazonaws-china.com/cn/about-aws/whats-new/2020/08/announcing-general-availability-of-bottlerocket/
GitHub
GitHub - bottlerocket-os/bottlerocket: An operating system designed for hosting containers
An operating system designed for hosting containers - bottlerocket-os/bottlerocket
【深圳垃圾分类正式进入“强制分类”时代】
从深圳市城市管理和综合执法局获悉，《深圳市生活垃圾分类管理条例》9月1日起正式实施，深圳垃圾分类由“倡议分类”进入“强制分类”，对未按规定分类投放生活垃圾并拒不改正的个人，最高处200元罚款；
对混合收集、运输已分类生活垃圾的收运单位，最高处50万元罚款。（新华社）
从深圳市城市管理和综合执法局获悉，《深圳市生活垃圾分类管理条例》9月1日起正式实施，深圳垃圾分类由“倡议分类”进入“强制分类”，对未按规定分类投放生活垃圾并拒不改正的个人，最高处200元罚款；
对混合收集、运输已分类生活垃圾的收运单位，最高处50万元罚款。（新华社）
韩国科学技术院并发和并行实验室 CS492 在线课程：并行程序的设计和分析（基于Rust）
课程目标：
本课程面向对并行计算机系统的现代理论和实践感兴趣的计算机科学（或相关学科）的高级本科生/研究生。 本课程旨在帮助此类学生：
1. 了解并发编程的动机和挑战
2. 学习并发程序的设计模式和推理原理
3. 设计，实施和评估并发程序
4. 将这些理解应用于实际的并行系统
该课程主要是讨论共享可变状态的最新理论及其在实际系统中的应用。
参考资料：
- 经典论文 - A Promising Semantics for Relaxed-Memory Concurrency ： https://sf.snu.ac.kr/promise-concurrency/
- Rust 社区明星并发库：crossbeam-rs
学习本课程需要的基础知识：
1. 数学（大一）：命题和证明
2. 数据结构（CS206）：链表，堆栈，队列
3. 系统编程（CS230）：内存布局，高速缓存，锁定
4. 编程语言（CS320）：Lambda演算，解释器
如果没有对这些主题的正确理解，您可能会在此课程中苦苦挣扎。
在本课程中可以帮助您的其他建议：
1. 对计算机体系结构的基本了解（CS311）
2. Rust编程经验
学习该课程要做的第一件事： https://github.com/kaist-cp/cs492-concur/issues/42 （当然这可以忽略，你没有学号无法登录该系统）
非该学校学生如何学习？
关注课程源码仓库： https://github.com/kaist-cp/cs492-concur
学习相关视频 ，会陆续上传： https://www.youtube.com/channel/UC8Jmj0869byUnsSRu_F5m9A
课程 slides： https://docs.google.com/presentation/d/1NMg08N1LUNDPuMxNZ-UMbdH13p8LXgMM3esbWRMowhU/edit#slide=id.p
homework占 60% 的评分比重，那说明homework更重要，可以重点关注源码仓库里的homework 目录。
课程目标：
本课程面向对并行计算机系统的现代理论和实践感兴趣的计算机科学（或相关学科）的高级本科生/研究生。 本课程旨在帮助此类学生：
1. 了解并发编程的动机和挑战
2. 学习并发程序的设计模式和推理原理
3. 设计，实施和评估并发程序
4. 将这些理解应用于实际的并行系统
该课程主要是讨论共享可变状态的最新理论及其在实际系统中的应用。
参考资料：
- 经典论文 - A Promising Semantics for Relaxed-Memory Concurrency ： https://sf.snu.ac.kr/promise-concurrency/
- Rust 社区明星并发库：crossbeam-rs
学习本课程需要的基础知识：
1. 数学（大一）：命题和证明
2. 数据结构（CS206）：链表，堆栈，队列
3. 系统编程（CS230）：内存布局，高速缓存，锁定
4. 编程语言（CS320）：Lambda演算，解释器
如果没有对这些主题的正确理解，您可能会在此课程中苦苦挣扎。
在本课程中可以帮助您的其他建议：
1. 对计算机体系结构的基本了解（CS311）
2. Rust编程经验
学习该课程要做的第一件事： https://github.com/kaist-cp/cs492-concur/issues/42 （当然这可以忽略，你没有学号无法登录该系统）
非该学校学生如何学习？
关注课程源码仓库： https://github.com/kaist-cp/cs492-concur
学习相关视频 ，会陆续上传： https://www.youtube.com/channel/UC8Jmj0869byUnsSRu_F5m9A
课程 slides： https://docs.google.com/presentation/d/1NMg08N1LUNDPuMxNZ-UMbdH13p8LXgMM3esbWRMowhU/edit#slide=id.p
homework占 60% 的评分比重，那说明homework更重要，可以重点关注源码仓库里的homework 目录。
2020 年度 Neuralink 的发布会上马斯克演示了一台用于为大脑植入芯片“LINK V0.9”的原型机；发布会现场，一头被植入芯片的猪被被用于演示，可以得知芯片可以检测大脑的运动信号并预测关节的运动，实际运动与预测非常拟合。
在此之前一直存在着侵入式和非侵入式脑机之争，Neuralink 公司已经尝试在各种动物身上进行试验通过了技术认证，包括老鼠、猴子、山羊；下一步想进行人体实验，但是由于美国的监管严格，公司希望在中国或俄罗斯进行。
