在逻辑门上运行Rust
本文将讨论许多话题，从CPU架构设计到历史上的诡异事件。喝一杯吧，接下来就是下坡路了。
尽管自90年代以来，这个数字已经稳步下降，但现在仍然有许多不同的、不兼容的CPU架构在使用。大多数计算机使用x86_64，几乎所有的移动设备和最近的Mac都使用某种基于ARM64的ISA（指令集架构）。
不过在特定领域，还有更多奇特的：大多数路由器仍然使用MIPS（由于历史原因），一屋子的开发人员使用RISC-V，PS3使用PowerPC，20年前的一些服务器使用Itanium，当然，IBM仍然在销售他们基于S/390的大型机（现在改名为z/Architecture）。嵌入式世界的产品就更多了。AVR（用于Arduino）、SuperH（土星、Dreamcast、卡西欧9860计算器），以及可敬的8051，一个1980年的英特尔芯片，现在仍在生产、销售，甚至由第三方扩展。
所有这些架构的定义特征都不同，主要的特征有
- 字大小：8、16、31、32、64位，有时更多
- 设计风格：RISC（指令少，操作简单），CISC（指令多，执行复杂的操作，VLIW（指令长，同时并行做很多事情）
- 存储器结构：哈佛（独立的代码存储器和数据存储器），冯-诺伊曼（共享）。
- 许可费用：RISC-V是开放的，可以免费使用，而X86和ARM等则需要许可费
- 广义上，它们的功能集：浮点数（x87）、加密（AES-NI）、支持本地高级字节码执行（Jazelle、AVR32B）、矢量计算（SSE、AVX、AltiVec）。
这还不算DSP架构，轻描淡写地说，它们是ISA的暮光之城（支持奇怪的算术运算、奇特的数据大小等）。
更多内容: https://zdimension.fr/crabs-all-the-way-down/
在Tokio Bytes上使用Kani Rust校验器
在这篇文章中，我们将介绍一个应用Kani Rust验证器（简称Kani，这是我们的开源形式验证工具，可以证明Rust代码的属性）到Tokio的一个例子。
Tokio是Rust程序的异步运行时，这意味着它将语言的低级异步功能抽象为有用的构建块（例如为异步任务的调度和执行提供一个执行器）。Tokio的目的是提供 "编写网络程序所需的构件，[具有]针对各种系统的灵活性，从具有几十个内核的大型服务器到小型嵌入式设备"。在这篇文章中，我们将关注Tokio堆栈的一个底层组件和证明一个核心数据结构的属性。
关于 Kani：
Kani Rust验证器是一个用于Rust的位精确模型检查器。
Kani对于验证Rust中的不安全代码特别有用，因为许多语言的常规保证不再由编译器检查。Kani可以验证
- 内存安全（例如，空指针解除引用）。
- 用户指定的断言（例如，
assert!(...)）。 - 没有恐慌（例如，对
None使用unwrap()）。 - 不存在某些类型的意外行为（例如，算术溢出）
博文: https://model-checking.github.io/kani-verifier-blog/2022/08/17/using-the-kani-rust-verifier-on-tokio-bytes.html
This Week in Rust 456
新一期的 Rust 周报速递发布，快来看看有哪些内容你曾经关注过 :)
This Week in Rust 456: https://this-week-in-rust.org/blog/2022/08/17/this-week-in-rust-456/
From 日报小组 Cupnfish
社区学习交流平台订阅：
评论区
写评论还没有评论