Follow.is Feed Verification
This message is used to verify that this feed (feedId:68119418071751680) belongs to me (userId:67570460419266560). Join me in enjoying the next generation information browser https://follow.is.
此博客中的热门博文
Specifying Systems 第五章笔记
5.1 内存的接口 本节通过一个规范表示接口，不涉及实现，也即不涉及判断真假的具体公式。 首先选择抽象的层级，第二章把“发送”操作用三个变量（ val 、 rdy 、 ack ）进行描述，并把 val 和 rdy 同时更改表示为一个原子操作。本章把“发送”操作用一个变量进行描述： val 。 接口试图规定“发送”操作是某一类 动作 ，这需要描述怎样的 动作 是符合本接口的，类似于在“函数是一等公民”的编程语言中描述函数。但 TLA+ 只能把 CONSTANT 、 VARIABLE 定义的变量作为模块的参数，而不能把 动作 定义的公式作为模块的参数。作为替代，TLA+ 中可以定义运算符以达到这个目的。把 动作 涉及的 N 个变量列举出来，定义一个 N 元运算符 CONSTANTS operator_as_action(_, _, _, _) 即可。 运算符的返回值不限定类型，而 动作 是一个公式，返回值是布尔型，所以还需要一个表示类型的假设 ASSUME \A p1, p2, p3, p4 : operator_as_action(p1, p2, p3, p4) \in BOOLEAN 在学习了需要的语法知识后，我们可以定义内存的规范了。 -------------------------- MODULE MemoryInterface --------------------------- VARIABLE memInt \* represent memory CONSTANTS Send(_, _, _, _), Reply(_, _, _, _), InitMemInt, \* set of possible initial values of memInt Proc, \* set of processor identiers Adr, \* set of memory addresses Val \* se...
将博客部署到星际文件系统（IPFS）
以持续集成的方式将你的博客部署到 IPFS 上，拥抱去中心化和 Web 3.0 🌎！ [1] 在 这篇文章中，我将主要介绍如何将你的 静态 博客以持续集成的方式部署到星际文件系统 IPFS 上，也会简单介绍一下 IPFS 的使用。本文中，我使用的 SSG [2] 是 Hugo ，使用的持续集成服务由 Netlify 提供，博客的源码可以在 GitHub 上找到。另，提醒一下，与 零网 一样，IPFS 默认 不匿名 👓，且对 Tor 的支持 还在开发中 。 前言 一年前的昨天🧐，知名的互联网基础设施服务提供商 Cloudflare 宣布 开始支持 IPFS Gateway，作为其 分布式互联网网关 项目的一部分。关于分布式互联网（Distributed Web，以下简称 D 网），它的到来很有可能会将我们带向 Web 3.0 时代，一个全新的互联网时代！而 D 网所具有的去中心化将会带我们走向新的自由之路——无审查，无高墙。👉🌎🌍🌏💫 起因 浏览 Twitter 时发现了 @GoHugoIO 的一条 推文 ，IPFS 四个字母激起了我的兴趣🐭（之前 轻微 了解过，印象只限于这四个字母），快速浏览一遍 链接的文章 之后，去看了他之前写的一篇 详细教程 ，打开 IPFS 的 官网 ，决定这次一定要尝试一下 IPFS！🕳️🦆 正文 文章的正文分为两个部分：持续集成和原生部署，第一部分是文章的主体，第二部分供感兴趣的读者研究。 当你按照此文章将博客成功部署到 IPFS 上后，你的博客将： ⚡拥有全球范围的高速 CDN，国内也有不错的访问速度（Cloudflare） 🌤️无需支出且永远在线（如果你不需要域名的话） 🛸走向未来 持续集成 如果你只是想直接通过持续集成的方式部署博客，那么你是无需在自己的电脑（本地）上安装 IPFS 的，你甚至可以完全不用接触 IPFS。但是，你的电脑必须安装 Git 和 Node.js 。如果你是一个程序员或之前有尝试过搭建静态博客，那么你对它们应该并不陌生。 准备环境 首先是 Git，我们要将博客所在的文...
评论
发表评论