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
12clh_lock_t big_kernel_lock ALIGN(L1_CACHE_LINE_SIZE);
13
14BOOT_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