RTOS/seL4
1
0
Fork 0
forked from Imagelibrary/seL4
Code Pull Requests Activity

mcs: SCs in the same region have the same size

Browse Source 
Although it is true that any SC that refers to the same location in
memory will have the same size, it is difficult to prove. This
explicitly checks to remove the burden of proof.

This approach is already used when determining whether two CNodes refer
to the same region.

Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This commit is contained in:
Curtis Millar
2020-04-01 11:43:25 +11:00
committed by Kent McLeod
parent 36e5d119e5
commit fb4dc44965
1 changed files with 4 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
src/object/objecttype.c
View File

@@ -353,8 +353,10 @@ bool_t CONST sameRegionAs(cap_t cap_a, cap_t cap_b)
#ifdef CONFIG_KERNEL_MCS
case cap_sched_context_cap:
if (cap_get_capType(cap_b) == cap_sched_context_cap) {
return cap_sched_context_cap_get_capSCPtr(cap_a) ==
cap_sched_context_cap_get_capSCPtr(cap_b);
return (cap_sched_context_cap_get_capSCPtr(cap_a) ==
cap_sched_context_cap_get_capSCPtr(cap_b)) &&
(cap_sched_context_cap_get_capSCSizeBits(cap_a) ==
cap_sched_context_cap_get_capSCSizeBits(cap_b));
}
break;
case cap_sched_control_cap: