File size: 1,585 Bytes
29f097e 32b4893 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 | -- SPDX-License-Identifier: LicenseRef-Sovereign-Leviathan-SL-AGPL3-001
-- Copyright (C) 2026 SNAPKITTYWEST / Sovereign Kernel Project
-- CLONE_GATE: sparse-router-formal::formal::scoring
import SparseRouter.Types
namespace SparseRouter.Scoring
open SparseRouter
def locality (w : Worker) (t : Task) : Int :=
if w.lastRegion = t.memoryRegion.val then 100 else 0
def memoryAffinity (w : Worker) (t : Task) : Int :=
if w.cacheFootprint = 0 then 50
else if w.lastRegion = t.memoryRegion.val then (t.cacheLinesHot : Int) * 10
else 0
def queuePressure (w : Worker) : Int :=
if w.deque.count = 0 then 80
else if w.deque.count < DequeCapacity / 4 then 40
else if w.deque.count < DequeCapacity / 2 then 0
else -40
def stealability (w : Worker) : Int :=
if w.deque.count > 2 then 20 else 0
def migrationCost (w : Worker) (t : Task) : Int :=
if w.lastRegion = t.memoryRegion.val then 0
else (t.footprintBytes : Int) / (1024 * 64)
def computeScore (w : Worker) (t : Task) : Int :=
locality w t + memoryAffinity w t + queuePressure w t +
stealability w t - migrationCost w t
theorem score_locality_bonus (w : Worker) (t : Task)
(h : w.lastRegion = t.memoryRegion.val) :
locality w t = 100 := by
simp [locality, h]
theorem score_empty_queue_bonus (w : Worker) (t : Task)
(h : w.deque.count = 0) :
queuePressure w = 80 := by
simp [queuePressure, h]
theorem score_no_migration_when_local (w : Worker) (t : Task)
(h : w.lastRegion = t.memoryRegion.val) :
migrationCost w t = 0 := by
simp [migrationCost, h]
end SparseRouter.Scoring
|