rCore OS
Replies: 39 comments 1 reply
-
|
2335周报 1、本周进展：
2、下周计划： 继续阅读Linux相关代码，阅读文章项目JUXTA代码，理清文章思路。 |
Beta Was this translation helpful? Give feedback.
-
|
linux代码不用深入理解分析，大致能读懂就好。现在还是要深入理解论文，最好能重现juxta这个project。
|
Beta Was this translation helpful? Give feedback.
-
|
在传统研究领域（就是上面的论文和其它一些相关论文），判断两个函数在语义上是否等价,可以考虑使用形式化验证技术。主要的步骤包括:
利用形式化方法去证明两个函数的行为一致性,是判断语义等价的有效途径。需要注意函数副作用的差异。此外还可以辅助测试典型用例,综合判断函数语义是否等价。但形式化验证技术对学生需要掌握的知识要求比较高。 也许我们可以考虑用最近兴起的代码理解技术来判断两个函数的语义等价性,而不一定需要形式验证。大致的具体操作包括:
相比形式验证,这种基于语义向量的函数对比可以更加自动化和泛化。随着预训练语言模型等技术的进步,这种判断语义等价的方法也会越来越准确可靠。但这一块我还不够熟悉，也许同学可以看看最新的AI方面的研究，获得相应启发。 注意，我们的研究可能不仅仅是函数，而是函数组成的一个模块，这也进一步加大了难度。即使要用AI技术，我觉得也是从传统的fuzzing/symbolic execution来入门为好。 |
Beta Was this translation helpful? Give feedback.
-
会议纪要时间2023.09.05 11:00~12:00 人员advisor: cy,zfx
内容
|
Beta Was this translation helpful? Give feedback.
-
|
论文补充： https://congyu-liu.github.io/assets/slides/kit_asplos23_slides.pdf |
Beta Was this translation helpful? Give feedback.
-
|
2336周报 1、本周进展：
2、下周计划：
|
Beta Was this translation helpful? Give feedback.
-
|
2337周报 1、本周进展：
2、下周计划：
|
Beta Was this translation helpful? Give feedback.
-
|
2338周报 1、本周进展：
2、下周计划：
|
Beta Was this translation helpful? Give feedback.
-
|
2339周报 1、本周进展：
2、下周计划：
|
Beta Was this translation helpful? Give feedback.
-
|
2341周报 1、本周进展：
2、下周计划：
|
Beta Was this translation helpful? Give feedback.
-
|
2342周报 1、本周进展：
2、下周计划：
|
Beta Was this translation helpful? Give feedback.
-
|
2343周报 1、本周进展：
2、下周计划：
|
Beta Was this translation helpful? Give feedback.
-
|
2344周报 1、本周进展：
2、下周计划：
|
Beta Was this translation helpful? Give feedback.
-
|
2345周报 1、本周进展：
2、下周计划：
|
Beta Was this translation helpful? Give feedback.
-
|
2346周报 1、本周进展：
2、下周计划：
|
Beta Was this translation helpful? Give feedback.
-
|
2347周报 1、本周进展：
2、下周计划：
|
Beta Was this translation helpful? Give feedback.
-
|
2409周报 1、本周进展：
2、下周计划：
|
Beta Was this translation helpful? Give feedback.
-
|
2410周报
本周新冠 + 心包积液，进展较慢 2、下周计划：
|
Beta Was this translation helpful? Give feedback.
-
|
2411周报
1、本周进展：
2、下周计划：
|
Beta Was this translation helpful? Give feedback.
-
|
2412周报 1、本周进展：
2、下周计划：
|
Beta Was this translation helpful? Give feedback.
-
|
2413周报
2、下周计划：
|
Beta Was this translation helpful? Give feedback.
-
|
2415周报
1、本周进展：
2、下周计划：
|
Beta Was this translation helpful? Give feedback.
-
|
1、本周进展
2、下周计划
|
Beta Was this translation helpful? Give feedback.
-
|
2417周报 1、本周进展
2、下周计划
|
Beta Was this translation helpful? Give feedback.
-
|
2420周报 1、本周进展：
2、下周计划：
|
Beta Was this translation helpful? Give feedback.
-
|
2421周报 1、本周进展：
2、下周计划：
|
Beta Was this translation helpful? Give feedback.
-
|
2422周报 1、本周进展
fn main() -> () {
let mut _0: (); // return place in scope 0 at src/main.rs:1:11: 1:11
let mut _1: std::vec::Vec<i32>; // in scope 0 at src/main.rs:2:9: 2:14
let mut _2: std::boxed::Box<[i32]>; // in scope 0 at /home/rust/library/alloc/src/macros.rs:49:52: 49:65
let mut _3: std::boxed::Box<[i32; 5]>; // in scope 0 at /home/rust/library/alloc/src/macros.rs:49:52: 49:65
let mut _4: std::boxed::Box<[i32; 5]>; // in scope 0 at /home/rust/library/alloc/src/macros.rs:49:52: 49:65
scope 1 {
debug a => _1; // in scope 1 at src/main.rs:2:9: 2:14
}
bb0: {
StorageLive(_1); // scope 0 at src/main.rs:2:9: 2:14
StorageLive(_2); // scope 0 at /home/rust/library/alloc/src/macros.rs:49:52: 49:65
StorageLive(_3); // scope 0 at /home/rust/library/alloc/src/macros.rs:49:52: 49:65
StorageLive(_4); // scope 0 at /home/rust/library/alloc/src/macros.rs:49:52: 49:65
_4 = Box([i32; 5]); // scope 0 at /home/rust/library/alloc/src/macros.rs:49:52: 49:65
(*_4) = [const 1_i32, const 2_i32, const 3_i32, const 4_i32, const 5_i32]; // scope 0 at /home/rust/library/alloc/src/macros.rs:49:56: 49:65
_3 = move _4; // scope 0 at /home/rust/library/alloc/src/macros.rs:49:52: 49:65
_2 = move _3 as std::boxed::Box<[i32]> (Pointer(Unsize)); // scope 0 at /home/rust/library/alloc/src/macros.rs:49:52: 49:65
StorageDead(_4); // scope 0 at /home/rust/library/alloc/src/macros.rs:49:64: 49:65
StorageDead(_3); // scope 0 at /home/rust/library/alloc/src/macros.rs:49:64: 49:65
_1 = slice::<impl [i32]>::into_vec::<std::alloc::Global>(move _2) -> bb1; // scope 0 at /home/rust/library/alloc/src/macros.rs:49:36: 49:66
// mir::Constant
// + span: /home/rust/library/alloc/src/macros.rs:49:36: 49:51
// + user_ty: UserType(0)
// + literal: Const { ty: fn(std::boxed::Box<[i32]>) -> std::vec::Vec<i32> {std::slice::<impl [i32]>::into_vec::<std::alloc::Global>}, val: Value(Scalar(<ZST>)) }
}
bb1: {
StorageDead(_2); // scope 0 at /home/rust/library/alloc/src/macros.rs:49:65: 49:66
drop(_1) -> bb2; // scope 0 at src/main.rs:12:1: 12:2
}
bb2: {
StorageDead(_1); // scope 0 at src/main.rs:12:1: 12:2
return; // scope 0 at src/main.rs:12:2: 12:2
}
}变成了 fn main() -> () {
let mut _0: (); // return place in scope 0 at src/main.rs:1:11: 1:11
let mut _1: std::vec::Vec<i32>; // in scope 0 at src/main.rs:2:9: 2:14
let mut _2: std::boxed::Box<[i32]>; // in scope 0 at /home/rust-9.26/library/alloc/src/macros.rs:49:52: 49:65
let mut _3: std::boxed::Box<[i32; 5]>; // in scope 0 at /home/rust-9.26/library/alloc/src/macros.rs:49:52: 49:65
let mut _4: usize; // in scope 0 at /home/rust-9.26/library/alloc/src/macros.rs:49:52: 49:65
let mut _5: usize; // in scope 0 at /home/rust-9.26/library/alloc/src/macros.rs:49:52: 49:65
let mut _6: *mut u8; // in scope 0 at /home/rust-9.26/library/alloc/src/macros.rs:49:52: 49:65
let mut _7: std::boxed::Box<[i32; 5]>; // in scope 0 at /home/rust-9.26/library/alloc/src/macros.rs:49:52: 49:65
scope 1 {
debug a => _1; // in scope 1 at src/main.rs:2:9: 2:14
}
scope 2 {
}
bb0: {
StorageLive(_1); // scope 0 at src/main.rs:2:9: 2:14
StorageLive(_2); // scope 0 at /home/rust-9.26/library/alloc/src/macros.rs:49:52: 49:65
StorageLive(_3); // scope 0 at /home/rust-9.26/library/alloc/src/macros.rs:49:52: 49:65
_4 = const 20_usize; // scope 2 at /home/rust-9.26/library/alloc/src/macros.rs:49:52: 49:65
_5 = const 4_usize; // scope 2 at /home/rust-9.26/library/alloc/src/macros.rs:49:52: 49:65
_6 = alloc::alloc::exchange_malloc(move _4, move _5) -> bb1; // scope 2 at /home/rust-9.26/library/alloc/src/macros.rs:49:52: 49:65
// mir::Constant
// + span: /home/rust-9.26/library/alloc/src/macros.rs:49:52: 49:65
// + literal: Const { ty: unsafe fn(usize, usize) -> *mut u8 {alloc::alloc::exchange_malloc}, val: Value(Scalar(<ZST>)) }
}
bb1: {
StorageLive(_7); // scope 0 at /home/rust-9.26/library/alloc/src/macros.rs:49:52: 49:65
_7 = ShallowInitBox(move _6, [i32; 5]); // scope 0 at /home/rust-9.26/library/alloc/src/macros.rs:49:52: 49:65
(*_7) = [const 1_i32, const 2_i32, const 3_i32, const 4_i32, const 5_i32]; // scope 0 at /home/rust-9.26/library/alloc/src/macros.rs:49:56: 49:65
_3 = move _7; // scope 0 at /home/rust-9.26/library/alloc/src/macros.rs:49:52: 49:65
_2 = move _3 as std::boxed::Box<[i32]> (Pointer(Unsize)); // scope 0 at /home/rust-9.26/library/alloc/src/macros.rs:49:52: 49:65
StorageDead(_7); // scope 0 at /home/rust-9.26/library/alloc/src/macros.rs:49:64: 49:65
StorageDead(_3); // scope 0 at /home/rust-9.26/library/alloc/src/macros.rs:49:64: 49:65
_1 = slice::<impl [i32]>::into_vec::<std::alloc::Global>(move _2) -> bb2; // scope 0 at /home/rust-9.26/library/alloc/src/macros.rs:49:36: 49:66
// mir::Constant
// + span: /home/rust-9.26/library/alloc/src/macros.rs:49:36: 49:51
// + user_ty: UserType(0)
// + literal: Const { ty: fn(std::boxed::Box<[i32]>) -> std::vec::Vec<i32> {std::slice::<impl [i32]>::into_vec::<std::alloc::Global>}, val: Value(Scalar(<ZST>)) }
}
bb2: {
StorageDead(_2); // scope 0 at /home/rust-9.26/library/alloc/src/macros.rs:49:65: 49:66
drop(_1) -> bb3; // scope 0 at src/main.rs:12:1: 12:2
}
bb3: {
StorageDead(_1); // scope 0 at src/main.rs:12:1: 12:2
return; // scope 0 at src/main.rs:12:2: 12:2
}
}但在实际执行中发现，始终未出现 猜测此问题是由 2、下周计划
|
Beta Was this translation helpful? Give feedback.
-
|
2426周报 1、本周进展
2、下周计划
|
Beta Was this translation helpful? Give feedback.
-
|
2427周报 1、本周进展
2、下周计划
|
Beta Was this translation helpful? Give feedback.
-
|
2428周报 1、本周进展
fn main() {
let a: &'static str;
{
let b = String::from("hello");
a = expand(&b);
}
println!("a: {a}");
}
fn expand<'a, 'b, T: ?Sized>(x: &'a T) -> &'b T{
fn helper<'a, 'b, T: ?Sized>(_va: &'a &'b (), vb: &'b T) -> &'a T{
vb
}
let f: fn(_, &'a T) -> &'b T = helper;
f(&&(), x)
// helper(&&(), x)
}2、下周计划
|
Beta Was this translation helpful? Give feedback.
-
|
2429周报 1、本周进展
2、下周计划
|
Beta Was this translation helpful? Give feedback.
-
目标：（学术研究类）分析比较具有同样对外接口但不同实现的内核模块差异性
基于组件模式构建内核模块会越来越多，对于某一个具体功能实现，可能有不少内核模块都能完成，且它们的对外接口相对固定，这时，需要分析这些内核模块的特征（独特性）、共性（差异性），用于发现潜在的bug，或者是便于选择内核模块，形成定制化OS。
参考：
注：偏学术研究类
如有兴趣一起来探索，请联系我 yuchen AT tsinghua.edu.cn OR 微信 id chyyuu
Beta Was this translation helpful? Give feedback.
All reactions