Regarding SMP and AMP in ThreadX

Question

I am starting a new project with STM32H747 which comes with cortex M4 and M7 dual cores. I know that STM32 Cude IDE provides support for Azure ThreadX directly, however, I am confused about the following in terms of multicore implementation of ThreadX:

1. When using SMP (Symmetric Multi-Processing), there is only one copy of the kernel/scheduler, in this case, how is it decided which core will the kernel run on? Obviously, the kernel will need to interrupt an ongoing thread on one of the cores, so is the core selected randomly or is there some other algorithm?
2. Can I use SMP for STM32H747 because even though the cores are different (M4 and M7), the instruction set architecture is the same ARMv7-M, so essentially, the same port can be used.
3. In case, SMP is not possible and I use AMP, can the native semaphore, mutex, and queue APIs be used to achieve proper synchronization?

Thanks,

Adhip