Check V programs against data races

[cristian-ilies-vasile]

We shall implement two fundamental laws of concurrency
1) Read Law: If I can read, no other go fn() can write.
2) Write Law: If I can write, no other go fn() can read.

I have an idea how to check all variables/objects versus all functions/ go routines in order of detecting at compile time data races. This action could be activated using a special compiler flag.

scope: create a graph with 2 types of nodes, and store it in tabular layout
a) only one node for object
b) go function nodes, all functions who process the variable of point a) over a know time frame

Example
obj_a => go fn1() => go fn2() => go fn3() => go fn4()
obj_b => go fn20() => go fn21() => go fn22() => go fn44()

// interleaved tree of go fn() and regular fn()
obj_c => go fn101() => fn102() => fn78() => fn99() => go fn21() => go fn22() => go fn44()

First step is to fill he following data structure (DATA STRUCTURE OF ALL VARs AND ALL GO FUNCTIONS)

field id	1
field name	FILE_NAME
type	string
example	nbody.v

field id	2
field name	TIME_FRAME_ID
type	Integer (unique)
example	2463

Comments:
Each program is divided in time frames, all user space threads (go fn()) run in a unique time frame.
time frame start = first program line under main function where go fn() is read
time frame end = first program line after last go fn() is read
Group all calls to user space threads before a wait() function is detected
We assign a unique ID to a directed acyclic graph build with all go functions able to run in parallel/concurrent.

fn main() {
go fn1_root() // 1st concurrent time frame is starting here
go fn_matrix_mul()
wg.wait() // 1st concurrent time frame is ending here
}

fn1_root() {
go fn2()
}

fn2() {
go fn3()
}

fn3() {
go fn4()
}

fn4() {

}

In scope are the following go functions
fn1_root()
fn2()
fn3()
fn4()
fn_matrix_mul()

field id	3
field name	OBJECT_ID
type	integer (unique)
example	1498528

Comments:
each variable/object get assigned a unique ID;
cannot be 2 objects with the same ID computed for all V modules & files in scope

field id	4
field name	OBJECT_NAME
type	string
example	m / nr_users / perimeter / i / j / k

Comments:
can be more than 2 objects having the same name

field id	5
field name	OBJECT_TYPE
type	string
example	i64 / pointer / string / array / struct

field id	6
field name	OBJECT_CAPABILITY
type	string
example	‘mut’ / ‘RW’ or 'val’ / ‘RO’

Comments:
each object is linked to mutable / immutable status

field id	7
field name	FN_GO
type	string / flag Y or N
example	N

Comments:
Mark each function in order to know if would run in concurrent mode or not

field id	8
field name	FN_NAME
type	string (unique)
example	arr_momentum (function name)

field id	9
field name	FN_OBJECT_NAME
type	string
example	g / x / m / user / wg / p_matrix

Comments:
name of the object taken from function definition
for a function with 3 parameters, will be 3 records, one for each parameter

field id	10
field name	FN_OBJECT_CAPABILITY
type	string
example	‘mut’ / ‘RW’ or ‘val’ / ‘RO’

Comments:
object capability taken from function definition

field id	11
field name	FN_OBJECT_MASK
type	string
example	p_a1 (code p_a1 := &a1 - define a pointer to object )

Comments:
pointer/reference to object find inside function

field id	12
field name	FN_OBJECT_IS_WRITTEN
type	String / flag Y or N

Comments:
If object is written inside the function
a = 25
a++
a--
in general seek for object on left side of ‘=’

field id	13
field name	NEXT_FN_NAME
type	string (unique)
example	print_automaton

Comments:
the next function in chain where first var of principal function is used
the smallest granularity is at variable level, should create a linked chain of functions with root as variable

I did a small PoC using SQL, on V other approach is needed
Check invalid combinations of objects vs functions capability

-- https://www.browserling.com/tools/all-hashes
-- https://sqliteonline.com/

WITH A1_W (
  FILE_NAME,                    -- 1
  TIME_FRAME_ID,                -- 2 
  OBJECT_ID,                    -- 3
  OBJECT_NAME,                  -- 4
  OBJECT_TYPE,                  -- 5
  OBJECT_CAPABILITY,            -- 6
  FN_GO,                        -- 7
  FN_NAME,                      -- 8
  FN_OBJECT_NAME,               -- 9
  FN_OBJECT_CAPABILITY,         -- 10 
  FN_OBJECT_MASK,               -- 11
  FN_OBJECT_IS_WRITTEN,         -- 12
  NEXT_FN_NAME)                 -- 13
  AS (
 SELECT 'nbody.v', 2463, 8899, 'a', 'i64', 'mut', 'Y', 'fn1',  'x_a1',  'mut', '',     'N', 'x_a11' UNION
 SELECT 'nbody.v', 2463, 8899, 'a', 'i64', 'mut', 'Y', 'fn11', 'x_a11', 'mut', '',     'Y', 'x_a12' UNION
 SELECT 'nbody.v', 2463, 8899, 'a', 'i64', 'mut', 'Y', 'fn12', 'x_a12', 'mut', 'p_a1', 'Y', 'x_a13' UNION
 SELECT 'nbody.v', 2463, 8899, 'a', 'i64', 'mut', 'Y', 'fn13', 'x_a13', 'mut', '',     'N', '-1'    UNION   
 SELECT 'nbody.v', 2463, 7744, 'b', 'i64', 'val', 'Y', 'fn2',  'x_b2',  'mut', '',     'Y', '-1'
  )
  
 /* 
  *    Query1
  *    check all combinations of objects vs functions capability
  *    OBJECT_CAPABILITY    FUNCTION_OBJECT_CAPABILITY
  *    'val'                'val'    // valid & safe
  *    'val'                'mut'    // invalid   
  *    'mut'                'val'    // valid
  *    'mut'                'mut'    // valid & dangerous
  */
 
 SELECT  
     PRINCIPAL_W.*
 FROM          A1_W PRINCIPAL_W
 WHERE 1=1
     AND PRINCIPAL_W.FN_GO = 'Y'                                                      -- only go fn() 
     AND PRINCIPAL_W.OBJECT_CAPABILITY    = 'val'
     AND PRINCIPAL_W.FN_OBJECT_CAPABILITY = 'mut'

Will return variable 7744 used on function fn2 get an error - impedance mismatch between object definition and how is defined on function signature.

Following query will find all objects having data race issues.

/* 
 *    Query2
 *    check all mutable objects written in multiple functions
 */

, Q2_W AS (
SELECT
     FILE_NAME
    ,TIME_FRAME_ID
    ,OBJECT_ID
    ,FN_NAME
  FROM (
  SELECT  
     COUNT(*) OVER (PARTITION BY FILE_NAME, TIME_FRAME_ID, OBJECT_ID,  FN_NAME) AS COUNT_BY_FN
    ,COUNT(*) OVER (PARTITION BY FILE_NAME, TIME_FRAME_ID, OBJECT_ID )          AS COUNT_BY_OBJECT
    ,FILE_NAME
    ,TIME_FRAME_ID
    ,OBJECT_ID
    ,FN_NAME
 FROM    A1_W PRINCIPAL_W
WHERE 1=1
     AND PRINCIPAL_W.FN_GO = 'Y'                                                      -- only go fn() 
     AND PRINCIPAL_W.OBJECT_CAPABILITY    = 'mut'
     AND PRINCIPAL_W.FN_OBJECT_CAPABILITY = 'mut'
     AND PRINCIPAL_W.FN_OBJECT_IS_WRITTEN = 'Y'
)
WHERE COUNT_BY_OBJECT > 1
) 

-- SELECT * FROM Q2_W

SELECT  
     PRINCIPAL_W.FILE_NAME,
     PRINCIPAL_W.OBJECT_NAME,
     PRINCIPAL_W.FN_NAME
 FROM           A1_W PRINCIPAL_W
     INNER JOIN Q2_W    ON PRINCIPAL_W.FILE_NAME = Q2_W.FILE_NAME
	               AND PRINCIPAL_W.TIME_FRAME_ID = Q2_W.TIME_FRAME_ID
                       AND PRINCIPAL_W.OBJECT_ID = Q2_W.OBJECT_ID 
                       AND PRINCIPAL_W.FN_NAME = Q2_W.FN_NAME
WHERE 1=1

FILE_NAME	OBJECT_NAME	FN_NAME
nbody.v	a	fn11
nbody.v	a	fn12

[cristian-ilies-vasile]

According with @krolaw dynamic creation of threads from a loop is the Achilles.
Consider threads a,b and c. a and c would race, but only a and b or b and c run together based on various if conditions.

Indeed, threads launched at run time dynamically based on a decision matrix(if then else) will be analyzed based on static graph layout and might trigger false positive actions.
In this case a, b and c will get marked as having data race issues.

// TO DO
o add START_TIME_FRAME & END_TIME_FRAME fields based on Line of Code index taken from file source code.
Useful for further investigations / check that each TIME_FRAME was computed with 100% accuracy

o add a new field FN_GO as a flag (Y / N) and extend the framework to all objects and functions.
-- done

o cannot alter the value of an object declared immutable by 'contract'/ function signature

/* 
 *    Query3
 *    check that the following combinations does not exists anymore  
 *    OBJECT_CAPABILITY    FUNCTION_OBJECT_CAPABILITY    FN_OBJECT_IS_WRITTEN
 *    'mut'                'val'                         'Y'    // invalid 
 */

special case(s)
//1 go function() without parameters and inside that function there is at least one pointer to object!
Such a function shall be inserted in DATA STRUCTURE OF ALL VARs AND ALL GO FUNCTIONS

//2 do not allow multiple pointers to the same object, with 'val' ref. capability inside any go fn()
one pointer per go fn() shall be maximum allowed.