Merge pull request #70 from seanwevans/claude/semaphore-invariant

Enforce the semaphore count <= max_count invariant

Author: seanwevans

Makefile

@@ -14,6 +14,7 @@ REGRESS = pg_os_basic \
           load_unload_module \
           modules \
           locks_security \
+          semaphore_validation
           schema_install
 REGRESS_OPTS = --outputdir=$(CURDIR)/tmp_pg_os_regress
 PGXS := $(shell $(PG_CONFIG) --pgxs)

expected/semaphore_validation.out

@@ -0,0 +1,27 @@
+-- create_semaphore must reject parameters that would violate the
+-- "0 <= count <= max_count, max_count >= 1" invariant.
+\set ECHO none
+SELECT create_semaphore('ok', 1, 2);
+ create_semaphore 
+------------------
+ 
+(1 row)
+
+SELECT name, count, max_count FROM semaphores WHERE name = 'ok';
+ name | count | max_count 
+------+-------+-----------
+ ok   |     1 |         2
+(1 row)
+
+SELECT create_semaphore('too_many', 5, 1);
+ERROR:  Semaphore initial count 5 must be between 0 and the maximum 1
+SELECT create_semaphore('negative', -1, 2);
+ERROR:  Semaphore initial count -1 must be between 0 and the maximum 2
+SELECT create_semaphore('no_max', 0, 0);
+ERROR:  Semaphore maximum must be at least 1 (got 0)
+SELECT count(*) AS semaphore_count FROM semaphores;
+ semaphore_count 
+-----------------
+               1
+(1 row)
+

pg_os--1.0.sql

@@ -462,7 +462,9 @@ CREATE TABLE IF NOT EXISTS semaphores (
     id SERIAL PRIMARY KEY,
     name TEXT UNIQUE NOT NULL,
     count INTEGER NOT NULL CHECK (count >= 0),
-    max_count INTEGER NOT NULL CHECK (max_count >= 1)
+    max_count INTEGER NOT NULL CHECK (max_count >= 1),
+    -- a semaphore can never hold more permits than its maximum
+    CHECK (count <= max_count)
 );
 
 
@@ -533,6 +535,13 @@ GRANT EXECUTE ON FUNCTION unlock_mutex(INTEGER, TEXT) TO PUBLIC;
 -- create a semaphore
 CREATE OR REPLACE FUNCTION create_semaphore(sem_name TEXT, initial_count INTEGER, max_val INTEGER) RETURNS VOID AS $$
 BEGIN
+    IF max_val < 1 THEN
+        RAISE EXCEPTION 'Semaphore maximum must be at least 1 (got %)', max_val;
+    END IF;
+    IF initial_count < 0 OR initial_count > max_val THEN
+        RAISE EXCEPTION 'Semaphore initial count % must be between 0 and the maximum %', initial_count, max_val;
+    END IF;
+
     INSERT INTO semaphores (name, count, max_count)
     VALUES (sem_name, initial_count, max_val);
 END;

sql/semaphore_validation.sql

@@ -0,0 +1,24 @@
+-- create_semaphore must reject parameters that would violate the
+-- "0 <= count <= max_count, max_count >= 1" invariant.
+\set ECHO none
+SET client_min_messages TO warning;
+DROP EXTENSION IF EXISTS pg_os CASCADE;
+CREATE EXTENSION pg_os;
+\set ECHO queries
+\set VERBOSITY terse
+
+-- a valid semaphore is accepted
+SELECT create_semaphore('ok', 1, 2);
+SELECT name, count, max_count FROM semaphores WHERE name = 'ok';
+
+\set ON_ERROR_STOP off
+-- initial count greater than the maximum is rejected
+SELECT create_semaphore('too_many', 5, 1);
+-- negative initial count is rejected
+SELECT create_semaphore('negative', -1, 2);
+-- a maximum below 1 is rejected
+SELECT create_semaphore('no_max', 0, 0);
+\set ON_ERROR_STOP on
+
+-- none of the invalid semaphores were created
+SELECT count(*) AS semaphore_count FROM semaphores;