+void update_os_arch_secondary_cores(uint8_t os_arch)
+{
+ u64 *table = get_spin_tbl_addr();
+ int i;
+
+ for (i = 1; i < CONFIG_MAX_CPUS; i++) {
+ if (os_arch == IH_ARCH_DEFAULT)
+ table[i * WORDS_PER_SPIN_TABLE_ENTRY +
+ SPIN_TABLE_ELEM_ARCH_COMP_IDX] = OS_ARCH_SAME;
+ else
+ table[i * WORDS_PER_SPIN_TABLE_ENTRY +
+ SPIN_TABLE_ELEM_ARCH_COMP_IDX] = OS_ARCH_DIFF;
+ }
+}
+