use std::io;
use std::sync::atomic::{AtomicI64, Ordering};
use crate::assertion_slots::MAX_ASSERTION_SLOTS;
use crate::shared_mem;
#[repr(C)]
pub struct EnergyBudget {
pub global_remaining: AtomicI64,
pub per_mark: [AtomicI64; MAX_ASSERTION_SLOTS],
pub per_mark_initial: i64,
pub realloc_pool: AtomicI64,
}
pub fn init_energy_budget(
global_energy: i64,
per_mark_initial: i64,
) -> Result<*mut EnergyBudget, io::Error> {
let ptr = shared_mem::alloc_shared(std::mem::size_of::<EnergyBudget>())?;
let budget = ptr as *mut EnergyBudget;
unsafe {
(*budget)
.global_remaining
.store(global_energy, Ordering::Relaxed);
(*budget).per_mark_initial = per_mark_initial;
}
Ok(budget)
}
pub unsafe fn init_mark_budget(budget: *mut EnergyBudget, slot_idx: usize) {
if slot_idx < MAX_ASSERTION_SLOTS {
let b = unsafe { &*budget };
b.per_mark[slot_idx].store(b.per_mark_initial, Ordering::Relaxed);
}
}
pub unsafe fn decrement_mark_energy(budget: *mut EnergyBudget, slot_idx: usize) -> bool {
let b = unsafe { &*budget };
if b.global_remaining.fetch_sub(1, Ordering::Relaxed) <= 0 {
b.global_remaining.fetch_add(1, Ordering::Relaxed);
return false;
}
if slot_idx < MAX_ASSERTION_SLOTS {
if b.per_mark[slot_idx].fetch_sub(1, Ordering::Relaxed) > 0 {
return true;
}
b.per_mark[slot_idx].fetch_add(1, Ordering::Relaxed);
if b.realloc_pool.fetch_sub(1, Ordering::Relaxed) > 0 {
return true;
}
b.realloc_pool.fetch_add(1, Ordering::Relaxed);
}
b.global_remaining.fetch_add(1, Ordering::Relaxed);
false
}
pub unsafe fn reset_energy_budget(budget: *mut EnergyBudget, new_global_energy: i64) {
let b = unsafe { &*budget };
b.global_remaining
.store(new_global_energy, Ordering::Relaxed);
b.realloc_pool.store(0, Ordering::Relaxed);
for slot in &b.per_mark {
slot.store(0, Ordering::Relaxed);
}
}
pub unsafe fn return_mark_energy_to_pool(budget: *mut EnergyBudget, slot_idx: usize) {
if slot_idx < MAX_ASSERTION_SLOTS {
let b = unsafe { &*budget };
let remaining = b.per_mark[slot_idx].swap(0, Ordering::Relaxed);
if remaining > 0 {
b.realloc_pool.fetch_add(remaining, Ordering::Relaxed);
}
}
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn test_mark_budget_decrement_and_return() {
let ptr = init_energy_budget(100, 10).expect("init failed");
unsafe {
init_mark_budget(ptr, 0);
assert!(decrement_mark_energy(ptr, 0));
assert!(decrement_mark_energy(ptr, 0));
return_mark_energy_to_pool(ptr, 0);
let b = &*ptr;
assert_eq!(b.per_mark[0].load(Ordering::Relaxed), 0);
assert_eq!(b.realloc_pool.load(Ordering::Relaxed), 8);
shared_mem::free_shared(ptr as *mut u8, std::mem::size_of::<EnergyBudget>());
}
}
#[test]
fn test_productive_mark_draws_from_realloc() {
let ptr = init_energy_budget(100, 5).expect("init failed");
unsafe {
init_mark_budget(ptr, 0);
decrement_mark_energy(ptr, 0); return_mark_energy_to_pool(ptr, 0);
init_mark_budget(ptr, 1);
for _ in 0..5 {
assert!(decrement_mark_energy(ptr, 1));
}
assert!(decrement_mark_energy(ptr, 1));
let b = &*ptr;
assert_eq!(b.realloc_pool.load(Ordering::Relaxed), 3);
shared_mem::free_shared(ptr as *mut u8, std::mem::size_of::<EnergyBudget>());
}
}
#[test]
fn test_global_energy_exhaustion() {
let ptr = init_energy_budget(3, 100).expect("init failed");
unsafe {
init_mark_budget(ptr, 0);
assert!(decrement_mark_energy(ptr, 0));
assert!(decrement_mark_energy(ptr, 0));
assert!(decrement_mark_energy(ptr, 0));
assert!(!decrement_mark_energy(ptr, 0));
let b = &*ptr;
assert_eq!(b.global_remaining.load(Ordering::Relaxed), 0);
shared_mem::free_shared(ptr as *mut u8, std::mem::size_of::<EnergyBudget>());
}
}
#[test]
fn test_realloc_flow() {
let ptr = init_energy_budget(50, 5).expect("init failed");
unsafe {
init_mark_budget(ptr, 0);
decrement_mark_energy(ptr, 0);
return_mark_energy_to_pool(ptr, 0);
let b = &*ptr;
assert_eq!(b.realloc_pool.load(Ordering::Relaxed), 4);
init_mark_budget(ptr, 1);
for _ in 0..5 {
assert!(decrement_mark_energy(ptr, 1));
}
for _ in 0..3 {
assert!(decrement_mark_energy(ptr, 1));
}
assert_eq!(b.realloc_pool.load(Ordering::Relaxed), 1);
shared_mem::free_shared(ptr as *mut u8, std::mem::size_of::<EnergyBudget>());
}
}
}