Alloy Tutorial（3）Traces Modelling —— Cache Memory

news2024/11/24 9:08:19

文章目录

  • Cache Memory
  • 完整代码

Cache Memory

//Addresses and data
sig Addr {}
sig Data {}

//A cache system consists of main memory and cached memory, but mapping addresses to data
one sig CacheSystem {
	var main, cache: Addr -> lone Data
}

//Initially there is no memory allocated
pred init [c: CacheSystem] {
	no c.main + c.cache
}

//Write data to a specified address in the cache
pred write [c : CacheSystem, a: Addr, d: Data] {
	c.main' = c.main
	c.cache' = c.cache ++ a -> d
}

//Read data from a specified address in the cache
pred read [c: CacheSystem, a: Addr, d: Data] {
	some d
	d = c.cache [a]
        c.main' = c.main
        c.cache' = c.cache
}

//Load some data from the main memory in the cache
//Note that this is non-deterministic: it does not specific what to load. This is left to the implementation
pred load [c : CacheSystem] {
	some addrs: set c.main.Data - c.cache.Data |
		c.cache' = c.cache ++ addrs <: c.main
	c.main' = c.main
}

//Flush memory from the cache back into the main memory.
//Note this is also non-deterministic
pred flush [c : CacheSystem] {
	some addrs: some c.cache.Data {
		c.main' = c.main ++ addrs <: c.cache
		c.cache' = c.cache - addrs -> Data
	}
}

//If a load is performed between a write and a read, this should not be observable.
//That is, if we perform the sequence: read, write, load, and read, 
//then reading the same address in both reads should return the same value,
//unless the write in between overwrote that value (i.e. a1=a2)
assert LoadNotObservable {
	all c : CacheSystem, a1, a2: Addr, d1, d2, d3: Data |
		{
		read [c, a2, d2];
		write [c, a1, d1];
		load [c];
		read [c, a2, d3]
		} implies d3 = (a1=a2 => d1 else d2)
	}

assert LoadPreserves{
	all c: CacheSystem | load[c] => c.main'=c.main
}

assert CannotReadInitially{
	all c: CacheSystem, a: Addr, d: Data | init[c] => not read[c, a, d]
}

pred destroy[c: CacheSystem, a: Addr]{
	c.main' = c.main - (a -> Data)
	c.cache' = c.cache - (a -> Data)
}

assert OnlyOneMemoryDestroyed{
	all c: CacheSystem, a: Addr | (destroy[c, a] => c.main'=c.main-(a->Data) and c.cache'=c.cache) 
	or (destroy[c, a] =>  c.cache'=c.cache-(a->Data) and c.main' = c.main)
}
//check LoadNotObservable for 5
//check LoadPreserves
//check CannotReadInitially
check OnlyOneMemoryDestroyed

In this workshop we will investigate checking whether the cache system satisfies the following invariant: No memory address is present in both the cache and the main memory.
Write a predicate inv that encodes this property.

  • 这里有两种写法：

    pred Inv[c: CacheSystem]{
	all a: Addr | (a in c.main.Data => a not in c.cache.Data) and (a in c.cache.Data => a not in c.main.Data)
}

    pred Inv2[c: CacheSystem] {
  // for a relation r : A -> B, r.B is a relational join that gives us the domain of r
  no (c.cache.Data & c.main.Data)
}

  • 本质思想是一样的，c.cache.Data 会拿到所有 cache 中的 Address，同样的 c.main.Data 也会拿到所有 main 中的 address，核心的思想是，一个 address a 如果出现在 c.main 中，那么就还一定不能出现在 c.cache 中，反之亦然。

  • 为了验证这两种写法是否相同，我还写了一个 assertion

    assert InvEqual{
	all c: CacheSystem | 
	Inv[c] <=> Inv2[c]
}
check InvEqual

  • 没有 counterexample 代表结果完全相同。

题目：We can use Alloy to help us reason about whether this invariant will always hold, by getting it to check two things:

  • (a) The initial state satisfies the invariant.
  • (b) Each operation preserves the invariant.

The cache system has the operations: write, read, load, and flush.
Write assertions to specify the two conditions above. Note that for the second condition we usually encode it as a collection of assertions: one for each of the operations.
Use Alloy to check these assertions. Which operations preserve the invariant and which don’t? Examine the counter-examples that Alloy finds to understand why certain operations don’t preserve the invariant. What are the smallest bounds for which the counter-examples show up?


assert writeInvariant{
	all c: CacheSystem, a:Addr, d:Data | Inv[c] and write[c, a, d] => after(Inv[c]) 
}

check writeInvariant
  • writeInvariant 是有 counter example 的
assert readInvariant{
	 all c: CacheSystem, a:Addr, d:Data | Inv[c] and read[c, a, d] => after(Inv[c]) 
}
check readInvariant
  • readInvariant 没有 counter example
assert loadInvariant{
	all c: CacheSystem | Inv[c] and  load[c] => after(Inv[c]) 
}

check loadInvariant
  • loadInvariant 是有 counter example 的
assert flushInvariant{
	all c: CacheSystem | Inv[c] and  flush[c] => after(Inv[c]) 
}
check flushInvariant
  • flushInvariant 没有 counter example

反例最小范围：

  • Alloy工具通过寻找反例来验证模型的断言。给定一个断言，Alloy尝试寻找一个实例，即一个特定的模型状态，使得断言不成立。这个实例被称为一个反例。
  • 然而，对于一个给定的断言，可能存在多个反例。Alloy默认的策略是寻找尽可能小的反例。“最小范围"这个概念是指，为了找到反例，Alloy搜索的模型状态空间的大小。例如，如果你有一个涉及整数的断言，Alloy可能会在一个范围内搜索可能的整数值，如-10到10。这个范围就是搜索的"范围”。"最小范围"是指能找到反例的最小的搜索范围。
  • 寻找最小范围的反例可以有助于更好地理解断言为什么会失败，因为这可以消除不必要的复杂性，并帮助你专注于导致断言失败的核心原因。

题目：Given that some of the operations don’t preserve the invariant, we can expect that from the initial state the system could reach a state in which the invariant doesn’t hold. However, the checks above don’t tell us what this sequence of operations might be. We will use Alloy to generate such a sequence of operations by modelling traces of transitions.

Write a fact first init that states that the first state in the trace is an initial state, i.e. satisfies the init predicate. Then write a fact trans that states that it is always the case that either one of the cache system operations occurs or the state remains unchanged. Hint: You should write a predicate that specifies what it means for the cache system state to remain unchanged during a transition and use that predicate in your fact.

题目解析：这两段话是在讨论如何用Alloy模型来生成操作序列，这些操作序列可以从初始状态开始，并可能导致一个违反不变性条件的状态。

  • 因为上面的题目中有些 assertion 可以找到 counter example 这就代表这些过程违反了 不变性
  • 这就意味着从初始状态开始，系统可能从某一个 state 开始会到达一个不满足不变性的状态。
  • 通俗来说，我们的程序是一系列状态的转变，从初始状态 s 0 s_0 s0​ 开始，这整个状态转变的序列我们称为 trace，其中我们不知道经过哪个 state 的时候就不满足 不变性了，然而，前面的检查并不能告诉我们导致这种结果的操作序列是什么。所以作者建议使用Alloy来生成这样的操作序列，方法是对状态转移的轨迹进行建模。
  • 第二段给出了两个任务。首先，要编写一个fact，命名为first init，该fact声明轨迹中的第一个状态是一个初始状态 s 0 s_0 s0​，即满足init谓词。接着，要编写一个名为trans的fact，该fact声明在任何时候，都应满足以下条件：要么执行一个缓存系统操作（write, read, flush, load），要么状态保持不变。 这里需要编写一个谓词，来规定在转移过程中缓存系统状态保持不变的含义，然后在fact 中使用这个谓词。

总结一下，这两段话的主要内容是：在Alloy模型中，我们可以通过建立轨迹的模型，来生成可能导致违反不变性的操作序列。具体来说，我们需要定义两个fact，一个声明轨迹的初始状态，另一个声明在任何时候，要么进行一个操作，要么状态不变。

pred do_nothing[c: CacheSystem] {
  c.cache' = c.cache and c.main' = c.main
}

fact trans {
  always {
    all c: CacheSystem | 
     do_nothing[c] or 
     (some a: Addr, d: Data | write[c,a,d]) or 
     (some a: Addr, d: Data | read[c,a,d]) or 
     load[c] or 
     flush[c]
  }
}

问题：Write an assertion that says that it is always the case that the invariant holds. Use Alloy to check this assertion and to generate a trace in which the system starts in the initial state and then performs a sequence of operations to reach a state in which the invariant is violated.

  • 在文档中，已经定义了一个名为 Inv 的不变式（invariant），该不变式表明了一个地址不可能同时在 cache 和 main 中存在。为了断言这个不变式总是被保持，我们可以在 Alloy 中添加如下的断言：
assert alwaysInvHolds {
  always all c: CacheSystem | Inv[c]
}
check alwaysInvHolds
  • 然而，需要注意的是，如果这个断言被 Alloy 模型检查器验证为假，那么表示存在一种可能的情况（或者称之为一个反例），即系统从初始状态开始，经过一系列的操作后，到达了一个违反了不变式 Inv 的状态。

问题：After you add the first_init fact you might find that some of your earlier checks that produced counterexamples no longer do so. Specifically the checks that each operation preserves the invariant.
There are two ways to write these checks, in general, for a state type State (which in this workshop is the CacheMemory type) and an operation predicate op:
在这里插入图片描述
You should take one of the checks that produced a counter-example earlier and write it in each of the forms above. Work out which form produces the counter-example and which does not.
Think about why the first init fact prevents one of them from generating a counter-example but not
the other. What does this tell you about the meaning of these two ways of writing invariant preservation assertions, in trace-based Alloy models? (i.e. in models that model traces of operations, not just individual transitions).

问题解析：
这个问题关注的是如何编写能够保持不变量的检查（check）。给出了两种编写的方式，并询问你在给定初始化 fact 后，哪种方式会生成反例（即违反不变量的情况），哪种方式不会。
两种编写检查的方式分别是：

  • all s:State | inv[s] and op[s] => after inv[s]
  • always all s:State | inv[s] and op[s] => after inv[s]

这两种方式的差异在于 always 关键字。在 Alloy 中，always 表示的是 “总是” 的意思，意味着不仅是当前的状态满足条件，而且在所有的后续状态中，这个条件也会被满足。
问题希望你选择之前生成反例的一个检查，然后用这两种方式重新写一遍，看看哪种方式会生成反例，哪种方式不会。然后思考一下为什么给定初始化 fact 后，其中一种方式不能生成反例，而另一种方式可以。这个结果对你理解在基于轨迹的 Alloy 模型（即那些建模操作序列的模型，而不仅仅是单个的转换）中，这两种方式的含义有什么启示？

  • 初始化的 fact 强制了模型的初始状态必须满足某种条件。对于那种不使用 always 的检查，如果初始状态满足了这个 fact，那么这个检查就有可能不会生成反例，因为所有满足 fact 的状态都满足了不变量。而对于使用 always 的检查，即使初始状态满足了这个 fact，只要存在一个可能的后续状态违反了不变量，那么这个检查就会生成反例。
  • 这表明，在基于轨迹的 Alloy 模型中，使用 always 的检查可以帮助我们发现那些只有在一系列操作之后才能发现的问题，而不使用 always 的检查只能帮助我们发现在初始状态就能发现的问题。

完整代码

//Addresses and data
sig Addr {}
sig Data {}

//A cache system consists of main memory and cached memory, but mapping addresses to data
one sig CacheSystem {
	var main, cache: Addr -> lone Data
}

//Initially there is no memory allocated
pred init [c: CacheSystem] {
	no c.main + c.cache
}

//Write data to a specified address in the cache
pred write [c : CacheSystem, a: Addr, d: Data] {
	c.main' = c.main
	c.cache' = c.cache ++ a -> d
}

//Read data from a specified address in the cache
pred read [c: CacheSystem, a: Addr, d: Data] {
	some d
	d = c.cache [a]
        c.main' = c.main
        c.cache' = c.cache
}

//Load some data from the main memory in the cache
//Note that this is non-deterministic: it does not specific what to load. This is left to the implementation
//pred load [c : CacheSystem] {
//	some addrs: set c.main.Data - c.cache.Data |
//		c.cache' = c.cache ++ addrs <: c.main
//	c.main' = c.main
//}

pred load [c : CacheSystem] {
	some addrs: set c.main.Data - c.cache.Data |
		c.cache' = c.cache ++ addrs <: c.main
	c.main' = c.main
}

//Flush memory from the cache back into the main memory.
//Note this is also non-deterministic
pred flush [c : CacheSystem] {
	some addrs: some c.cache.Data {
		c.main' = c.main ++ addrs <: c.cache
		c.cache' = c.cache - addrs -> Data
	}
}

//If a load is performed between a write and a read, this should not be observable.
//That is, if we perform the sequence: read, write, load, and read, 
//then reading the same address in both reads should return the same value,
//unless the write in between overwrote that value (i.e. a1=a2)
assert LoadNotObservable {
	all c : CacheSystem, a1, a2: Addr, d1, d2, d3: Data |
		{
		read [c, a2, d2];
		write [c, a1, d1];
		load [c];
		read [c, a2, d3]
		} implies d3 = (a1=a2 => d1 else d2)
	}

assert LoadPreserves{
	all c: CacheSystem | load[c] => c.main'=c.main
}

assert CannotReadInitially{
	all c: CacheSystem, a: Addr, d: Data | init[c] => not read[c, a, d]
}

pred destroy[c: CacheSystem, a: Addr]{
	c.main' = c.main - (a -> Data)
	c.cache' = c.cache - (a -> Data)
}

assert OnlyOneMemoryDestroyed{
	all c: CacheSystem, a: Addr | (destroy[c, a] => c.main'=c.main-(a->Data) and c.cache'=c.cache) 
	or (destroy[c, a] =>  c.cache'=c.cache-(a->Data) and c.main' = c.main)
}


pred Inv[c: CacheSystem]{
	all a: Addr | (a in c.main.Data => a not in c.cache.Data) and (a in c.cache.Data => a not in c.main.Data)
}


pred Inv2[c: CacheSystem] {
  // for a relation r : A -> B, r.B is a relational join that gives us the domain of r
  no (c.cache.Data & c.main.Data)
  // alternatively we could write
  //all a: Addr | 
  //  (some c.cache[a] => no c.main[a]) and (some c.main[a] => no c.cache[a])
}


//check LoadNotObservable for 5
//check LoadPreserves
//check CannotReadInitially
//check OnlyOneMemoryDestroyed

assert InvEqual{
	all c: CacheSystem | 
	Inv[c] <=> Inv2[c]
}


assert initInvariant {
  all c: CacheSystem | init[c] => Inv[c]
}


assert writeInvariant{
	always all c: CacheSystem, a:Addr, d:Data | Inv[c] and write[c, a, d] => after(Inv[c]) 
}


assert readInvariant{
	 all c: CacheSystem, a:Addr, d:Data | Inv[c] and read[c, a, d] => after(Inv[c]) 
}


assert loadInvariant{
	all c: CacheSystem | Inv[c] and  load[c] => after(Inv[c]) 
}

assert flushInvariant{
	all c: CacheSystem | Inv[c] and  flush[c] => after(Inv[c]) 
}

fact first_init{
	all c: CacheSystem | init[c]
}
//
//fact trans{
//	always all c: CacheSystem | 
//	// 保持不变
//	c.main' = c.main and c.cache' = c.cache
//	// 进行一些操作
//	or (some a: Addr, d: Data | read[c, a, d])
//	or (some a: Addr, d: Data | write[c, a, d])
//	or load[c]
//	or flush[c]
//}


pred do_nothing[c: CacheSystem] {
  c.cache' = c.cache and c.main' = c.main
}

fact trans {
  always {
    all c: CacheSystem | 
     do_nothing[c] or 
     (some a: Addr, d: Data | write[c,a,d]) or 
     (some a: Addr, d: Data | read[c,a,d]) or 
     load[c] or 
     flush[c]
  }
}

check initInvariant
//check flushInvariant
//check loadInvariant
//check readInvariant
//check writeInvariant

//check InvEqual

本文来自互联网用户投稿，该文观点仅代表作者本人，不代表本站立场。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如若转载，请注明出处：http://www.coloradmin.cn/o/635835.html

如若内容造成侵权/违法违规/事实不符，请联系多彩编程网进行投诉反馈，一经查实，立即删除！

相关文章

yolov5——从未见过注释比代码还多的源码解析You Only Look Once And You get it——训练部分

yolov5——从未见过注释比代码还多的源码解析You Only Look Once And You get it——训练部分

目录 一&#xff1a;前言 二&#xff1a;先介绍v5源码中必须知道的一些文件&#xff08;了解的可直接加入第三代码部分&#xff09; ​编辑 三&#xff1a;训练 参数配置 模式选择 搭建网络 加载预训练和自定义模型的参数 是否需要冻结层数 定义累计梯度的次数 设置…
阅读更多...
零基础小白如何自学 Unity 游戏开发？(送 Unity 教程)

零基础小白如何自学 Unity 游戏开发？(送 Unity 教程)

如何自学 Unity&#xff1f;初级阶段&#xff1a;学习编程语言初级阶段&#xff1a;编程实践中级阶段&#xff1a;继续学习编程语言 Unity 教程赠书活动内容简介作者简介赠书方式 如何自学 Unity&#xff1f; 有很多同学对 游戏开发 很感兴趣&#xff0c;但都不知道从何学起&a…
阅读更多...
PostgreSQL如何查看事务所占有的锁？

PostgreSQL如何查看事务所占有的锁？

表级锁命令LOCK TABLE 在PG中&#xff0c;显式地在表上加锁的命令为“LOCK TABLE”&#xff0c;此命令的语法如下&#xff1a; LOCK [TABLE] [ONLY] name [,...][IN lockmode MODE] [NOWAIT]语法中各项参数说明如下&#xff1a; name&#xff1a;表名lockmode&#xff1a;表…
阅读更多...
GPT1，2，3

GPT1，2，3

GPT1 transformer解码器因为有掩码所以不看后面的东西 gpt就是transformer的解码器&#xff0c;bert 是transformer的编码器 gpt核心卖点&#xff1a;不管输入如何&#xff0c;transformer模型不会变 半监督&#xff1a;先在没有标号上进行训练&#xff0c;再到有标号上进行微…
阅读更多...
配置Nexus私服

配置Nexus私服

私服是一种特殊的远程仓库&#xff0c;它代理广域网上的远程仓库&#xff0c;供局域网下的maven用户使用。 目前Nexus3的官方下载地址为 https://help.sonatype.com/repomanager3/product-information/download &#xff0c;由于下载较慢&#xff08;真的很慢&#xff09;&…
阅读更多...
【MySQL】库和表的增删查改

【MySQL】库和表的增删查改

目录 一、库的操作 1、创建数据库 2、数据库所使用的编码 2.1查询编码集和校验集 2.2查看数据库的字符集和校验集 2.3创建数据库指定字符集和校验集 2.4不同的校验集所筛选的数据结果不一样 3、查看数据库 4、修改数据库 5、删除数据库 6、数据库的备份和恢复 6.1备…
阅读更多...
数字图像处理期末复习习题 SCUEC part2

数字图像处理期末复习习题 SCUEC part2

1.连续图像在空间位置上的离散化称为采样&#xff1b;图像空间分辨率由灰度级决定。 2.坐标的离散化叫采样&#xff0c;幅值的离散化叫量化。 3. 4.图像分割方法多种多样&#xff0c;一般可以根据像素灰度取值的特性将分割方法分为两类&#xff08;阈值分割&#xff0c;区域分割…
阅读更多...
软件工程开发文档写作教程(15)—概要设计书的编写

软件工程开发文档写作教程(15)—概要设计书的编写

本文原创作者&#xff1a;谷哥的小弟作者博客地址&#xff1a;http://blog.csdn.net/lfdfhl本文参考资料&#xff1a;电子工业出版社《软件文档写作教程》 马平&#xff0c;黄冬梅编著 概要设计书的编写 按照国家《概要设计说明书GB8567—88&#xff09;所定义的标准&#xff0…
阅读更多...
算法刷题-链表-链表相交

算法刷题-链表-链表相交

链表相交 面试题 02.07. 链表相交思路其他语言版本JavaPythonGojavaScript 面试题 02.07. 链表相交 同&#xff1a;160.链表相交 力扣题目链接 给你两个单链表的头节点 headA 和 headB &#xff0c;请你找出并返回两个单链表相交的起始节点。如果两个链表没有交点&#xff0…
阅读更多...
chatgpt赋能python：Python如何填充空值

chatgpt赋能python：Python如何填充空值

Python如何填充空值 在数据处理过程中&#xff0c;经常会遇到数据集中存在空值的情况。这些空值&#xff08;或缺失值&#xff09;可能会影响数据分析的准确性&#xff0c;因此我们需要对这些空值进行填充。Python作为一种流行的编程语言&#xff0c;提供了许多有效的方法来处…
阅读更多...
【C++ 笔记四】STL 标准模板库 —— 容器基础

【C++ 笔记四】STL 标准模板库 —— 容器基础

【C 笔记四】STL 标准模板库 —— 容器基础 文章目录 【C 笔记四】STL 标准模板库 —— 容器基础I - 概述 STL1.1 - 范围与定义1.2 - 组成与关系1.3 - 实用举例 II - 概述容器2.1 - 迭代器2.2 - 容器的结构与分类2.3 - 序列式容器2.4 - 关联式容器2.5 - 不定序容器2.6 - 总述 I…
阅读更多...
.mdf.locked加密sql server完美恢复---惜分飞

.mdf.locked加密sql server完美恢复---惜分飞

有可能用友ERP软件的sql server 数据库所在机器被勒索病毒加密,扩展名为.locked和昨天恢复的基本类似(.locked加密勒索数据库级别恢复),通过分析确认sql server被这种病毒加密,也可以完美恢复 通过恢复之后数据库正常挂载成功 测试应用一切正常 对于类似这种被加密的勒索的数…
阅读更多...
【Python开发】FastAPI 10：SQLAlchemy 数据库操作

【Python开发】FastAPI 10：SQLAlchemy 数据库操作

在 FastAPI 中使用 SQL 数据库可以使用多个 ORM 工具&#xff0c;例如 SQLAlchemy、Tortoise ORM 等&#xff0c;类似 Java 的 Mybatis 。这些 ORM 工具可以帮助我们方便地与关系型数据库进行交互&#xff0c;如 MySQL 、PostgreSQL等。本篇文章将介绍如何使用 SQLAlchemy 来完…
阅读更多...
chatgpt赋能python：Python的安装方法

chatgpt赋能python：Python的安装方法

Python的安装方法 简介 Python是一种非常流行的编程语言&#xff0c;它可以用于多种应用场景。Python简单易懂&#xff0c;可读性强&#xff0c;易于维护。因此&#xff0c;它成为了数据科学家、软件工程师和Web开发者的首选编程语言之一。 安装环境 在安装Python之前&…
阅读更多...
【SpringBoot 3.x】整合Mybatis-Plus多数据源、Druid

【SpringBoot 3.x】整合Mybatis-Plus多数据源、Druid

本地开发环境说明 开发依赖版本Spring Boot3.0.6Mybatis-Plus3.5.3.1dynamic-datasource-spring-boot-starter3.6.1JDK20 pom.xml主要依赖 <dependencies><dependency><groupId>org.springframework.boot</groupId><artifactId>spring-boot-st…
阅读更多...
MIT 6.S081 Lab Two

MIT 6.S081 Lab Two

MIT 6.S081 Lab Two 引言system callsSystem call tracing&#xff08;moderate&#xff09;实验解析实现思路小结 Sysinfo&#xff08;moderate&#xff09;实验解析 可选的挑战 引言 本文为 MIT 6.S081 2020 操作系统 实验一解析。 MIT 6.S081课程前置基础参考: 基于RISC-V…
阅读更多...
【C++】图解类和对象（下）

【C++】图解类和对象（下）

图解类和对象&#xff08;下&#xff09; 文章目录 图解类和对象&#xff08;下&#xff09;一、初始化列表&#xff08;1&#xff09;定义&#xff08;2&#xff09;注意事项&#xff08;3&#xff09;explicit关键字&#xff08;4&#xff09;结论 二、static成员1.定义2.特性…
阅读更多...
windows一键安装redis7.0.11

windows一键安装redis7.0.11

下载 下载地址:https://gitcode.net/zengliguang/windows_redis7.0.11_offline_install.git 使用git进行进行clone下载 在电脑桌面或者其他文件夹下 &#xff0c;鼠标右键点击 选择git clone &#xff0c;下图中url为下载地址&#xff0c;Directory为本地存储路径&#xff…
阅读更多...
【瑞萨RA_FSP】常用存储器介绍

【瑞萨RA_FSP】常用存储器介绍

文章目录 一、存储器种类二、 RAM存储器1. DRAM1.1 SDRAM1.2 DDR SDRAM 2. SRAM3. DRAM与SRAM的应用场合 三、非易失性存储器1. ROM存储器1.1 MASK ROM1.2 OTPROM1.3 EPROM1.4 EEPROM 2. FLASH存储器 一、存储器种类 存储器是计算机结构的重要组成部分。存储器是用来存储程序代…
阅读更多...
电子科技大学编译原理复习笔记（九）：代码优化

电子科技大学编译原理复习笔记（九）：代码优化

阅读更多...
推荐文章
最新文章

Copyright @ 2022~2023