Some ARM-based single board computers combine two types of Cortex processors, for example 4 A73 and 4 A 53 or 2 A72 and 4 A53. How does FreeBSD schedule processes on these chips? Does it use all cores at random, only the "big" or "little" set, or something more complicated?