Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions loader/src/aarch64/el.c
Original file line number Diff line number Diff line change
Expand Up @@ -54,12 +54,14 @@ int ensure_correct_el(int logical_cpu)
} else {
LDR_PRINT("INFO", logical_cpu, "Resetting CNTVOFF\n");
asm volatile("msr cntvoff_el2, xzr");
asm volatile("isb" ::: "memory");
}
} else {
if (el == EL2) {
/* seL4 relies on the timer to be set to a useful value */
LDR_PRINT("INFO", logical_cpu, "Resetting CNTVOFF\n");
asm volatile("msr cntvoff_el2, xzr");
asm volatile("isb" ::: "memory");
LDR_PRINT("INFO", logical_cpu, "Dropping from EL2 to EL1\n");
switch_to_el1();
LDR_PRINT("INFO", logical_cpu, "CurrentEL=");
Expand Down
2 changes: 2 additions & 0 deletions loader/src/aarch64/exceptions.c
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,8 @@ void arch_set_exception_handler(void)
if (el != EL0) {
asm volatile("msr vbar_el1, %0" :: "r"(arm_vector_table));
}

asm volatile("isb" ::: "memory");
}

uintptr_t exception_register_state[32];
Expand Down
1 change: 1 addition & 0 deletions loader/src/aarch64/init.c
Original file line number Diff line number Diff line change
Expand Up @@ -130,6 +130,7 @@ void arch_jump_to_kernel(int logical_cpu)
{
/* seL4 always expects the current logical CPU number in TPIDR_EL1 */
asm volatile("msr TPIDR_EL1, %0" :: "r"(logical_cpu));
asm volatile("isb" ::: "memory");

((sel4_entry)(loader_data->kernel_entry))(
loader_data->ui_p_reg_start,
Expand Down
8 changes: 8 additions & 0 deletions loader/src/aarch64/util64.S
Original file line number Diff line number Diff line change
Expand Up @@ -249,6 +249,10 @@ BEGIN_FUNC(switch_to_el1)

/* set ELR so that it's possible to perform ERET */
msr elr_el2, x30

/* barrier for writes to special register */
isb
Comment on lines +252 to +254
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A bit nitpicky, but it are called "system registers" on AArch64 and the comment is vague enough that you can as well not have it, because if you understand the comment and why the ISB is there, you don't need the comment anyway.

However, because of the ERET below, it's much more important to say why an ISB may be needed after all, because usually it can be omitted in such cases.

The best documentation about this so far I found in the bloody glossary of ARM DDI 0487, under "Context Synchronization event". It says, other than returning from an exception being one:

The effects of a Context synchronization event are:

  • No instructions appearing in program order after an instruction that causes a Context
    synchronization event will have performed any part of their functionality until the Context
    synchronization event has occurred.
  • All direct and indirect writes to System registers that are made before the Context
    synchronization event affect any instruction, including a direct read, that appears
    in program order after the instruction causing the Context synchronization event.

To me it seems the instruction causing the context synchronisation event itself is excluded, and happens before the barrier so to speak. So changes to system registers spsr_el2 and elr_el2 which affect ERET behaviour do need an ISB.


eret
END_FUNC(switch_to_el1)

Expand All @@ -274,6 +278,10 @@ BEGIN_FUNC(switch_to_el2)

/* set ELR so RET returns to caller */
msr elr_el3, x30

/* barrier for writes to special register */
isb

eret
END_FUNC(switch_to_el2)

Expand Down