-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
10 changed files
with
238 additions
and
49 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -2,4 +2,6 @@ site/ | |
.DS_Store | ||
*.docx | ||
src/* | ||
*pycache* | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,60 @@ | ||
--- | ||
comments: true | ||
authors: | ||
- stormckey | ||
categories: | ||
- CS242 | ||
- PL | ||
date: 2023-12-09 | ||
nostatistics: true | ||
draft: true | ||
--- | ||
|
||
# CS242 Week 1 - Syntax and Semantics | ||
|
||
!!! abstract | ||
The lecture note in the website is very clear and condensed. However, the knowledge is organized in an intuitive instead of a neat way. Here I will try to list some important points for reference and some really intuitive pick-ups. | ||
|
||
<!-- more --> | ||
|
||
!!! info | ||
course version: 2019-fall | ||
|
||
course website: [:octicons-book-16:](https://stanford-cs242.github.io/f19/lectures/01-2-syntax-semantics) | ||
|
||
my assignment: [:octicons-mark-github-16:]() | ||
|
||
## The Idea of Backus's paper | ||
|
||
The first reading assignment was the paper of Backus,"Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs". I did not read through the whole paper but I have finished half of it. | ||
|
||
The main idea of the paper, I think, is that Backus tried to liberate the programmers from the laborious work required by Von Neumann languages, where programmers are busy handling the irrelevant details like memory management, variable assignment, nested control flow etc. So he proposed a new kind of system where no variable, assignment and history is needed. He gave the definition of the system and showed some convenient properties of the system such as we can analyse and transform the program in a algebra-like way. | ||
|
||
That's where I have read to. And as a student 50 years after the publication of the paper, I can conclude that the so said Von Neumann languages are still the mainstream today and the underlying hardware implementation is also monopolized by the Von Neumann architecture. | ||
|
||
I'm skeptical whether the method proposed by Backus a actually a better way, as all the laborious work seems also necessary to be done some way if we dont come up with a brand new architecture. And the ability to control this details may be necessay to control the computer efficiently, which is obviously an advantage over functional languages. | ||
|
||
So is the mechanism of Non Von Neumann languages really a practical and better way? How much power can it unleash? The answer remains unkonwn, at least to me.(Maybe this is problem that has already been solved somewhere) | ||
|
||
## Induction | ||
|
||
Lecture 1.2 validate the induction for natual numbers, here are things that I think is important: | ||
|
||
- every natual number is either 0 or a successor of natual number. So our case is exhaustive. | ||
- For any given n, we need always to find its predecessor until we find 0, the process of which will always terminate in finite steps. | ||
- This rule applies to other structures. So a good way to help us untangle our proof mechanism is to write down the structure. | ||
|
||
## Operational Semantics | ||
|
||
Here some quotations from TAPL which I think describe the operational semantics very well: | ||
|
||
> Operational semantics specifies the behavior of a programming language by defining a simple abstract machine for it. | ||
> For simple languages, a state of the machine is just a term, and the machine’s behavior is defined by a transition function that, for each state, either gives the next state by performing a step of simplification on the term or declares that the machine has halted. | ||
> The intuition is that, if t is the state of the abstract machine at a given moment, then the machine can make a step of computation and change its state to t′. | ||
|
||
|
||
|
||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,51 @@ | ||
--- | ||
comments: true | ||
authors: | ||
- stormckey | ||
categories: | ||
- CS242 | ||
- PL | ||
date: 2023-12-09 | ||
nostatistics: true | ||
draft: true | ||
--- | ||
|
||
# CS242 Week 2 - Lambda Calculus | ||
|
||
!!! abstract | ||
The lecture note in the website is very clear and condensed. However, the knowledge is organized in an intuitive instead of a neat way. Here I will try to list some important points for reference and some really intuitive pick-ups. | ||
|
||
<!-- more --> | ||
|
||
!!! info | ||
course version: 2019-fall | ||
|
||
course website: [:octicons-book-16:](https://stanford-cs242.github.io/f19/lectures/02-1-lambda-calculus) | ||
|
||
my assignment: [:octicons-mark-github-16:]() | ||
|
||
|
||
## Operational Semantics | ||
|
||
=== "D-Lam" | ||
|
||
$$\frac{\ }{\bf{\lambda} x . e \bf{val}}$$ | ||
|
||
<center> Functions are values. | ||
|
||
=== "D-App-Step" | ||
|
||
$$\frac{e_{lam} \mapsto e_{lam}'}{e_{lam} \ e_{arg} \mapsto e_{lam}' \ e_{arg}}$$ | ||
|
||
<center>Step the left expression $e_{lam}$ until it becomes a function. | ||
|
||
=== "D-App-Sub" | ||
|
||
$$\frac{\ }{(\bf{\lambda} x . e_{lam}) \ e_{arg} \mapsto [x \rightarrow e_{arg}]\ e_{lam}}$$ | ||
|
||
<center>replace all free variables x in $e_{lam}$ with $e_{arg}$. | ||
|
||
## Main Idea | ||
|
||
1. Understanding lambda calculus as an extendable and analyzable language. The following class could be abstracted as extending lambda calculus with some PL theories. | ||
2. To prove that we have enumerated all the edge cases, we need to prove the safety of the program after we prevent the renumerated cases. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,66 @@ | ||
--- | ||
comments: true | ||
authors: | ||
- stormckey | ||
categories: | ||
- OS | ||
- Lab | ||
date: 2023-12-10 | ||
nostatistics: true | ||
--- | ||
|
||
# 操作系统 - lab5 Demand Paging | ||
!!! abstract | ||
一些踩过的坑,以及一个 kernel 执行流程总结 | ||
<!-- more --> | ||
|
||
## kernel 执行流程 | ||
|
||
<div class="annotate" markdown> | ||
```title="kernel 执行流程" hl_lines="8 14-18" linenums="0" | ||
- `opensbi` 执行完毕 | ||
- `_start`: 完成 stvec, sie, mtimecmp, sstatus 和栈的设置,然后依次调用以下函数 | ||
- `setup_vm`: 填写页表 | ||
- `relocate`: 用设置好的页表修改 satp, 启动虚拟内存 | ||
- `mm_init`: 完成内存分配函数的初始化 | ||
- `setup_vm_final`: 切换到新的页表 | ||
- `task_init`: 初始化进程 | ||
- 对于 idle 以外的线程,在task_struct中添加stack和segment-01(1)对应的两段vma | ||
- `start_kernel`: 不进入 test 等时钟中断,而是直接调用 schedule 调度走 | ||
- `schedule`: 根据policy选择下一个要调度的线程,调用 switch_to 至该线程 | ||
- `switch_to`: 获取先后线程的PCB地址,调用__switch_to | ||
- `__switch_to`: 当前上下文存入 PCB,加载下一个进程的 PCB | ||
- `__dummy`: 切用户栈,sret 返回用户段,而 sepc 是我们初始化的时候就指定的的 USER_START | ||
- `ENTRY`: PC跳转至ENTRY,但是此时该页的映射并未完成,PAGE FAULT | ||
- `_traps`: PAGE FAULT,保存上下文进入trap_handler | ||
- `trap_handler`: 确认是PAGE FAULT后,调用do_page_fault | ||
- `do_page_fault`: 根据current的vma确认是段错误、文件页缺页还是匿名页缺页,分配新页,填写内容(2),填写页表,返回 | ||
- `_traps`: 恢复上下文返回,此后对应页已有映射 | ||
- `ENTRY`: 恢复执行,此后调度或者遇到新的缺页均同上处理 | ||
``` | ||
</div> | ||
|
||
1. 也即readelf时得到的segment-01,包括.text .rodata .bss | ||
2. 清零或者拷贝文件内容 | ||
|
||
## 栈切换问题 | ||
|
||
文档中指出,由用户发起的中断,我们需要在`_traps`开头切换到内核栈,但是对于内核发起的中断就不需要。而要判断中断是否由内核发起就要判断`sscratch`是否为0,在lab4中我把t0压栈后用t0来检验。 | ||
|
||
但是在lab5中这一方法行不通,因为当我们试图把t0压栈的时候我们的栈可能根本就是没分配的用户栈,那么这个压栈的行为只会引发新的PAGE FAULT,如此永远循环。 | ||
|
||
为了寻找解决方法可以先试图去查看linux时如何解决这一问题的,这是对应的[:octicons-code-16:代码](https://elixir.bootlin.com/linux/v6.0/source/arch/riscv/kernel/entry.S#L27) | ||
|
||
可以看到linux使用了tp(thread pointer)以及指令`csrwr`,前者倒不是必要的使用,我们主要关注到`csrwr`指令可以实现csr与其他寄存器的交换,从而我们sp与`sscratch`的切换就不需要其他寄存器了,这就是正确的解决方式。 | ||
|
||
## PAGE FAULT | ||
|
||
处理缺页异常时要仔细处理文件页的复制问题,如果要复制的一页中既有file_content,也有一些不在file之中的(如bss段),我们就需要分别处理这两段,前者复制,后者清零。 | ||
|
||
以下是一种处理思路: | ||
|
||
- 无论如何,清零新页 | ||
- 找到`bad_addr`所在页的开头和结尾为默认的拷贝起地址和终地址 | ||
- 起地址不应小于文件内容开头地址`vm_start` | ||
- 起地址不应大于文件内容结尾地址`vm_start + vm_content_size_in_file` | ||
- 终地址不应大于文件内容结尾地址`vm_start + vm_content_size_in_file` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,64 +1,57 @@ | ||
Babel==2.12.1 | ||
beautifulsoup4==4.11.2 | ||
cairocffi==1.4.0 | ||
CairoSVG==2.6.0 | ||
certifi==2022.12.7 | ||
cffi==1.15.1 | ||
charset-normalizer==3.0.1 | ||
click==8.1.3 | ||
Babel==2.13.1 | ||
cairocffi==1.6.1 | ||
CairoSVG==2.7.1 | ||
certifi==2023.11.17 | ||
cffi==1.16.0 | ||
charset-normalizer==3.3.2 | ||
click==8.1.7 | ||
colorama==0.4.6 | ||
csscompressor==0.9.5 | ||
cssselect2==0.7.0 | ||
defusedxml==0.7.1 | ||
et-xmlfile==1.1.0 | ||
ghp-import==2.1.0 | ||
gitdb==4.0.10 | ||
GitPython==3.1.31 | ||
htmlmin==0.1.12 | ||
idna==3.4 | ||
importlib-metadata==6.0.0 | ||
gitdb==4.0.11 | ||
GitPython==3.1.40 | ||
idna==3.6 | ||
importlib-metadata==7.0.0 | ||
jieba==0.42.1 | ||
Jinja2==3.1.2 | ||
jsmin==3.0.1 | ||
Markdown==3.3 | ||
markdown-meta-extension==0.5.3 | ||
markdown-toc==1.2.6 | ||
MarkupSafe==2.1.2 | ||
Markdown==3.5.1 | ||
MarkupSafe==2.1.3 | ||
mergedeep==1.3.4 | ||
mkdocs==1.4.2 | ||
mkdocs-blog-plugin==0.25 | ||
-e git+https://github.com/TonyCrane/mkdocs-changelog-plugin.git@b90ffb47c85e451dd82ce2b0d8779a0f35bea8a0#egg=mkdocs_changelog_plugin | ||
mkdocs-git-revision-date-localized-plugin==1.2.0 | ||
mkdocs-glightbox==0.3.2 | ||
mkdocs-material==9.1.0 | ||
mkdocs-material-extensions==1.1.1 | ||
mkdocs-meta-descriptions-plugin==2.2.0 | ||
mkdocs-minify-plugin==0.6.2 | ||
mkdocs==1.5.3 | ||
mkdocs-changelog-plugin==0.1.3 | ||
mkdocs-git-revision-date-localized-plugin==1.2.1 | ||
mkdocs-glightbox==0.3.5 | ||
mkdocs-macros-plugin==1.0.5 | ||
mkdocs-material==9.5.1 | ||
mkdocs-material-extensions==1.3.1 | ||
mkdocs-meta-manager==0.2.1 | ||
mkdocs-statistics-plugin==0.1.2 | ||
mkdocs-table-reader-plugin==2.0 | ||
mkdocs-table-reader-plugin==2.0.3 | ||
mkdocs-tooltips==0.1.0 | ||
numpy==1.24.2 | ||
openpyxl==3.1.1 | ||
packaging==23.0 | ||
pandas==1.5.3 | ||
pathvalidate==2.5.2 | ||
Pillow==9.4.0 | ||
numpy==1.26.2 | ||
packaging==23.2 | ||
paginate==0.5.6 | ||
pandas==2.1.4 | ||
pathspec==0.11.2 | ||
Pillow==10.1.0 | ||
platformdirs==4.1.0 | ||
pycparser==2.21 | ||
Pygments==2.14.0 | ||
pymdown-extensions==9.9.2 | ||
Pygments==2.17.2 | ||
pymdown-extensions==10.5 | ||
python-dateutil==2.8.2 | ||
pytz==2022.7.1 | ||
PyYAML==6.0 | ||
pytz==2023.3.post1 | ||
PyYAML==6.0.1 | ||
pyyaml_env_tag==0.1 | ||
regex==2022.10.31 | ||
requests==2.28.2 | ||
regex==2023.10.3 | ||
requests==2.31.0 | ||
six==1.16.0 | ||
smmap==5.0.0 | ||
soupsieve==2.4 | ||
smmap==5.0.1 | ||
tabulate==0.9.0 | ||
termcolor==2.4.0 | ||
tinycss2==1.2.1 | ||
toc==0.0.11 | ||
urllib3==1.26.14 | ||
watchdog==2.3.1 | ||
tzdata==2023.3 | ||
urllib3==2.1.0 | ||
watchdog==3.0.0 | ||
webencodings==0.5.1 | ||
zipp==3.15.0 | ||
zipp==3.17.0 |