Skip to content

Commit 93d5697

Browse files
jonlamb-ghjonlamb-gh
committed
Initial commit, new imx6/sabre project
1 parent 695141a commit 93d5697

12 files changed

+496
-0
lines changed

‎.gitignore

+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
/target
2+
**/*.rs.bk
3+
Cargo.lock
4+
/artifacts
5+
src/bin/root-task.rs

‎Cargo.toml

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
[package]
2+
name = "solox"
3+
version = "0.0.1"
4+
authors = ["jonlamb-gh <[email protected]>"]
5+
6+
[dependencies]
7+
libsel4-sys = {git = "https://github.com/jonlamb-gh/libsel4-sys.git", branch = "devel"}
8+
9+
[dependencies.wee_alloc]
10+
version = "0.4"
11+
features = ["static_array_backend"]
12+
optional = true
13+
14+
[dependencies.proptest]
15+
version = "0.8.5"
16+
default-features = false
17+
features = ["alloc", "nightly"]
18+
optional = true
19+
20+
[features]
21+
default = []
22+
alloc = ["wee_alloc"]
23+
test = ["alloc", "proptest"]

‎README.md

+9
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,11 @@
11
# solox-amp-rust
2+
23
AMP experiments in feL4 (seL4/Rust) on SoloX ARM SoC (A9 + M4)
4+
5+
The [Nitrogen6 SoloX][solox] SoC has both an A9 core and an M4 core.
6+
7+
The seL4 root task runs on the A9 core.
8+
9+
It first initializes the system, then runs a separate Rust application on the M4 core.
10+
11+
[solox]: https://boundarydevices.com/product/nit6_solox-imx6/

‎Xargo.toml

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
[target.x86_64-sel4-fel4.dependencies]
2+
alloc = {}
3+
[target.armv7-sel4-fel4.dependencies]
4+
alloc = {}
5+
[target.aarch64-sel4-fel4.dependencies]
6+
alloc = {}

‎fel4.toml

+167
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,167 @@
1+
[fel4]
2+
artifact-path = "artifacts"
3+
target-specs-path = "target_specs"
4+
target = "armv7-sel4-fel4"
5+
platform = "sabre"
6+
7+
[x86_64-sel4-fel4]
8+
BuildWithCommonSimulationSettings = true
9+
KernelOptimisation = "-O2"
10+
KernelVerificationBuild = false
11+
KernelBenchmarks = "none"
12+
KernelFastpath = true
13+
LibSel4FunctionAttributes = "public"
14+
KernelNumDomains = 1
15+
HardwareDebugAPI = false
16+
KernelFWholeProgram = false
17+
KernelResetChunkBits = 8
18+
LibSel4DebugAllocBufferEntries = 0
19+
LibSel4DebugFunctionInstrumentation = "none"
20+
KernelNumPriorities = 256
21+
KernelStackBits = 12
22+
KernelTimeSlice = 5
23+
KernelTimerTickMS = 2
24+
# the following keys are specific to x86_64-sel4-fel4 targets
25+
KernelArch = "x86"
26+
KernelX86Sel4Arch = "x86_64"
27+
KernelMaxNumNodes = 1
28+
KernelRetypeFanOutLimit = 256
29+
KernelRootCNodeSizeBits = 19
30+
KernelMaxNumBootinfoUntypedCaps = 230
31+
KernelSupportPCID = false
32+
KernelCacheLnSz = 64
33+
KernelDebugDisablePrefetchers = false
34+
KernelExportPMCUser = false
35+
KernelFPU = "FXSAVE"
36+
KernelFPUMaxRestoresSinceSwitch = 64
37+
KernelFSGSBase = "msr"
38+
KernelHugePage = true
39+
KernelIOMMU = false
40+
KernelIRQController = "IOAPIC"
41+
KernelIRQReporting = true
42+
KernelLAPICMode = "XAPIC"
43+
KernelMaxNumIOAPIC = 1
44+
KernelMaxNumWorkUnitsPerPreemption= 100
45+
KernelMultiboot1Header = true
46+
KernelMultiboot2Header = true
47+
KernelMultibootGFXMode = "none"
48+
KernelSkimWindow = true
49+
KernelSyscall = "syscall"
50+
KernelVTX = false
51+
KernelX86DangerousMSR = false
52+
KernelX86IBPBOnContextSwitch = false
53+
KernelX86IBRSMode = "ibrs_none"
54+
KernelX86RSBOnContextSwitch = false
55+
KernelXSaveSize = 576
56+
LinkPageSize = 4096
57+
UserLinkerGCSections = false
58+
59+
[x86_64-sel4-fel4.pc99]
60+
KernelX86MicroArch = "nehalem"
61+
LibPlatSupportX86ConsoleDevice = "com1"
62+
63+
[x86_64-sel4-fel4.debug]
64+
KernelDebugBuild = true
65+
KernelPrinting = true
66+
KernelColourPrinting = true
67+
KernelUserStackTraceLength = 16
68+
69+
[x86_64-sel4-fel4.release]
70+
KernelDebugBuild = false
71+
KernelPrinting = false
72+
73+
[armv7-sel4-fel4]
74+
BuildWithCommonSimulationSettings = true
75+
KernelOptimisation = "-O2"
76+
KernelVerificationBuild = false
77+
KernelBenchmarks = "none"
78+
KernelFastpath = true
79+
LibSel4FunctionAttributes = "public"
80+
KernelNumDomains = 1
81+
HardwareDebugAPI = false
82+
KernelFWholeProgram = false
83+
KernelResetChunkBits = 8
84+
LibSel4DebugAllocBufferEntries = 0
85+
LibSel4DebugFunctionInstrumentation = "none"
86+
KernelNumPriorities = 256
87+
KernelStackBits = 12
88+
KernelTimeSlice = 5
89+
KernelTimerTickMS = 2
90+
# the following keys are specific to armv7-sel4-fel4 targets
91+
KernelArch = "arm"
92+
KernelArmSel4Arch = "aarch32"
93+
KernelMaxNumNodes = 1
94+
KernelRetypeFanOutLimit = 256
95+
KernelRootCNodeSizeBits = 19
96+
KernelMaxNumBootinfoUntypedCaps = 230
97+
KernelAArch32FPUEnableContextSwitch = true
98+
KernelDebugDisableBranchPrediction = false
99+
KernelFPUMaxRestoresSinceSwitch = 64
100+
KernelIPCBufferLocation = "threadID_register"
101+
KernelMaxNumWorkUnitsPerPreemption = 100
102+
LinkPageSize = 4096
103+
UserLinkerGCSections = false
104+
105+
[armv7-sel4-fel4.debug]
106+
KernelDebugBuild = true
107+
KernelPrinting = true
108+
KernelColourPrinting = true
109+
KernelUserStackTraceLength = 16
110+
111+
[armv7-sel4-fel4.release]
112+
KernelDebugBuild = false
113+
KernelPrinting = false
114+
115+
[armv7-sel4-fel4.sabre]
116+
KernelARMPlatform = "sabre"
117+
ElfloaderImage = "elf"
118+
ElfloaderMode = "secure supervisor"
119+
ElfloaderErrata764369 = true
120+
KernelArmEnableA9Prefetcher = false
121+
KernelArmExportPMUUser = false
122+
KernelDebugDisableL2Cache = false
123+
124+
[aarch64-sel4-fel4]
125+
BuildWithCommonSimulationSettings = true
126+
KernelOptimisation = "-O2"
127+
KernelVerificationBuild = false
128+
KernelBenchmarks = "none"
129+
KernelFastpath = true
130+
LibSel4FunctionAttributes = "public"
131+
KernelNumDomains = 1
132+
HardwareDebugAPI = false
133+
KernelFWholeProgram = false
134+
KernelResetChunkBits = 8
135+
LibSel4DebugAllocBufferEntries = 0
136+
LibSel4DebugFunctionInstrumentation = "none"
137+
KernelNumPriorities = 256
138+
KernelStackBits = 12
139+
KernelTimeSlice = 5
140+
KernelTimerTickMS = 2
141+
# the following keys are specific to aarch64-sel4-fel4 targets
142+
KernelArch = "arm"
143+
KernelArmSel4Arch = "aarch64"
144+
KernelMaxNumNodes = 1
145+
KernelRetypeFanOutLimit = 256
146+
KernelRootCNodeSizeBits = 19
147+
KernelMaxNumBootinfoUntypedCaps = 230
148+
KernelDebugDisableBranchPrediction = false
149+
KernelFPUMaxRestoresSinceSwitch = 64
150+
KernelIPCBufferLocation = "threadID_register"
151+
KernelMaxNumWorkUnitsPerPreemption = 100
152+
LinkPageSize = 4096
153+
UserLinkerGCSections = false
154+
155+
[aarch64-sel4-fel4.debug]
156+
KernelDebugBuild = true
157+
KernelPrinting = true
158+
KernelColourPrinting = true
159+
KernelUserStackTraceLength = 16
160+
161+
[aarch64-sel4-fel4.release]
162+
KernelDebugBuild = false
163+
KernelPrinting = false
164+
165+
[aarch64-sel4-fel4.tx1]
166+
KernelARMPlatform = "tx1"
167+
ElfloaderImage = "binary"

‎rust-toolchain

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
nightly

‎src/fel4_test.rs

+145
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,145 @@
1+
use proptest::prelude::*;
2+
use proptest::test_runner::{TestCaseError, TestError, TestRunner};
3+
4+
use alloc::string::String;
5+
use core::fmt;
6+
#[cfg(feature = "KernelPrinting")]
7+
use sel4_sys::DebugOutHandle;
8+
use sel4_sys::*;
9+
10+
#[cfg(feature = "KernelPrinting")]
11+
macro_rules! debug_print {
12+
($($arg:tt)*) => ({
13+
use core::fmt::Write;
14+
DebugOutHandle.write_fmt(format_args!($($arg)*)).unwrap();
15+
});
16+
}
17+
18+
#[cfg(feature = "KernelPrinting")]
19+
macro_rules! debug_println {
20+
($fmt:expr) => (debug_print!(concat!($fmt, "\n")));
21+
($fmt:expr, $($arg:tt)*) => (debug_print!(concat!($fmt, "\n"), $($arg)*));
22+
}
23+
24+
#[cfg(feature = "KernelPrinting")]
25+
pub fn run() {
26+
debug_println!("\n\nrunning example tests");
27+
let mut runner = TestRunner::default();
28+
let mut num_passed = 0;
29+
let mut num_failed = 0;
30+
for found_success in [
31+
print_test_result(
32+
"test_message_info_predictability",
33+
test_message_info_predictability(&mut runner),
34+
),
35+
print_test_result(
36+
"test_cap_rights_predictability",
37+
test_cap_rights_predictability(&mut runner),
38+
),
39+
].iter()
40+
{
41+
if *found_success {
42+
num_passed += 1;
43+
} else {
44+
num_failed += 1;
45+
}
46+
}
47+
debug_println!(
48+
"test result: {}. {} passed; {} failed\n\n",
49+
if num_failed == 0 { "ok" } else { "FAILED" },
50+
num_passed,
51+
num_failed
52+
);
53+
halt();
54+
}
55+
56+
fn test_message_info_predictability(
57+
runner: &mut TestRunner,
58+
) -> Result<(), TestError<(u32, u32, u32, u32)>> {
59+
runner.run(
60+
&(0u32..0xfffff, 0u32..0x7, 0u32..0x3, 0u32..0x7f),
61+
|input| {
62+
let (label, caps, extra, length) = input;
63+
let (label, caps, extra, length) = (label as seL4_Word, caps as seL4_Word, extra as seL4_Word, length as seL4_Word);
64+
let out = unsafe {
65+
let msg = seL4_MessageInfo_new(label, caps, extra, length);
66+
let ptr = &msg as *const seL4_MessageInfo_t as *mut seL4_MessageInfo_t;
67+
(
68+
seL4_MessageInfo_ptr_get_label(ptr),
69+
seL4_MessageInfo_ptr_get_capsUnwrapped(ptr),
70+
seL4_MessageInfo_ptr_get_extraCaps(ptr),
71+
seL4_MessageInfo_ptr_get_length(ptr),
72+
)
73+
};
74+
let (out_label, out_caps, out_extra, out_length) = out;
75+
if label == out_label && caps == out_caps && extra == out_extra && length == out_length
76+
{
77+
Ok(())
78+
} else {
79+
Err(TestCaseError::fail(format!(
80+
"Mismatched input and output. {:?} vs {:?}",
81+
input, &out
82+
)))
83+
}
84+
},
85+
)
86+
}
87+
88+
fn test_cap_rights_predictability(
89+
runner: &mut TestRunner,
90+
) -> Result<(), TestError<(u32, u32, u32)>> {
91+
runner.run(&(0u32..2, 0u32..2, 0u32..2), |input| {
92+
let (grant, read, write) = input;
93+
let (grant, read, write) = (grant as seL4_Word, read as seL4_Word, write as seL4_Word);
94+
let out = unsafe {
95+
let msg = seL4_CapRights_new(grant, read, write);
96+
let ptr = &msg as *const seL4_CapRights_t as *mut seL4_CapRights_t;
97+
(
98+
seL4_CapRights_ptr_get_capAllowRead(ptr),
99+
seL4_CapRights_ptr_get_capAllowGrant(ptr),
100+
seL4_CapRights_ptr_get_capAllowWrite(ptr),
101+
)
102+
};
103+
let (out_grant, out_read, out_write) = out;
104+
if grant == out_grant && read == out_read && write == out_write {
105+
Ok(())
106+
} else {
107+
Err(TestCaseError::fail(format!(
108+
"Mismatched input and output. {:?} vs {:?}",
109+
input, &out
110+
)))
111+
}
112+
})
113+
}
114+
115+
/// Prints a summary of the test output.
116+
/// Returns true if the test succeeded, false otherwise.
117+
fn print_test_result<T: fmt::Debug>(
118+
test_name: &'static str,
119+
result: Result<(), TestError<T>>,
120+
) -> bool {
121+
match result {
122+
Ok(_) => {
123+
debug_println!("{} ... ok", test_name);
124+
true
125+
}
126+
Err(e) => {
127+
debug_println!("{} ... FAILED\n\t{}", test_name, e);
128+
false
129+
}
130+
}
131+
}
132+
133+
#[cfg(all(feature = "KernelDebugBuild", not(feature = "KernelPrinting")))]
134+
pub fn run() {
135+
halt();
136+
}
137+
138+
#[cfg(feature = "KernelDebugBuild")]
139+
fn halt() {
140+
unsafe { seL4_DebugHalt() };
141+
}
142+
#[cfg(not(feature = "KernelDebugBuild"))]
143+
fn halt() {
144+
panic!("Halting");
145+
}

0 commit comments

Comments
 (0)