1 /*
2  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3  *
4  * SPDX-License-Identifier: GPL-2.0-only
5  */
6 
7 #include <config.h>
8 #include <smp/lock.h>
9 
10 #ifdef ENABLE_SMP_SUPPORT
11 
12 clh_lock_t big_kernel_lock ALIGN(L1_CACHE_LINE_SIZE);
13 
clh_lock_init(void)14 BOOT_CODE void clh_lock_init(void)
15 {
16     for (int i = 0; i < CONFIG_MAX_NUM_NODES; i++) {
17         big_kernel_lock.node_owners[i].node = &big_kernel_lock.nodes[i];
18     }
19 
20     /* Initialize the CLH head */
21     big_kernel_lock.nodes[CONFIG_MAX_NUM_NODES].value = CLHState_Granted;
22     big_kernel_lock.head = &big_kernel_lock.nodes[CONFIG_MAX_NUM_NODES];
23 }
24 
25 #endif /* ENABLE_SMP_SUPPORT */
26