When null isn't just null -- value representation in ParaSail

The qualifier optional may be applied to any type in ParaSail, effectively producing a type with one additional value, namely the null value.  In many languages, null is only used for pointer types, and is often represented as a zero address.  In ParaSail, we want to be able to add the null value to any type without presuming that the zero value is available for that purpose, so this means that the representation for null will vary depending on the particular type.

For simple types, coming up with a null value is pretty straightforward.  For unsigned integer types, a value one greater than the maximum value could be used for null.   For example, given an unsigned type going from 0 to 100, the value 101 could be used to represent null.  Similarly, for enumeration types that use an internal unsigned integer representation, such as 0 for #false and 1 for #true, the null value could be represented by one more than the maximum internal unsigned integer code, for example 2 for the null value of an optional Boolean type.  For a signed integer type, one less than the minimum value might make sense, particularly on a 2's complement machine where there is one "extra" negative value anyway.  So for a 64-bit signed integer, one might use -2**63+1 .. 2**63-1 for "normal" values of the type, and reserve -2**63 for the null value.  Most floating point representations include the notion of "Not a Number" (NaN), and some NaN value would make sense for null.  Since there are no run-time checks in ParaSail (checking all being done at compile-time), it would be fine to use a "non-signaling" NaN for null.

For more complex types, the representation for null is a bit more interesting.  One common kind of type would be a simple "wrapper," that is, a type defined by a class that has exactly one var component.  For example:

class Box<Contents_Type is Assignable<>> is
    var Contents : Contents_Type;
  exports
    function Create(Value : Contents_Type) -> Box is
      return (Contents => Value);
    end function Create;
    ...
end class Box; 

In this case, it would be nice to have the wrapper type use exactly the same representation as that of the underlying component type (e.g. Contents_Type).  This would mean that the null value for the wrapper would be the same as the null value for the component type.  This does mean that the component type must not itself be marked as optional, as then there would be no way to distinguish the wrapper being non-null but containing a single null component, from the case where the wrapper itself is null.

So our conclusion is that a wrapper type can use the same representation as its component type so long as the component type is not itself marked optional.  If the component type is itself marked optional, then the wrapper needs to allow for its "own" representation for null, which might in some cases be accommodated by simply allowing for yet one more value if the component type is "simple," or a level of indirection for a more complex component type.

Now what about more complex types?  For example, a type defined by a class with multiple var components:

class Pair<Element_Type is Assignable<>> is
    var Left : Element_Type;
    var Right : Element_Type;
  exports
    function Cons(Left, Right : Element_Type) -> Pair is
      return (Left => Left, Right => Right);
    end function Cons;
    ...
end class Pair;  

One obvious representation for a type with multiple components is as a sequence of memory cells long enough to accommodate the representation of each of the components, and then some provision for representing null, which could be by piggy-backing on one of the components if it is not itself allowed to be null, or by adding an additional bit to indicate null-ness.  However, in our initial (prototype, ParaSail-Virtual-Machine-based) implementation, we have chosen to represent every object using a single 64-bit memory cell.  This basically means that if the value cannot fit in a single 64-bit cell, it will need to use a level of indirection.  To simplify further, we won't be doing any "packing" initially, so even if the components are each quite short (such as booleans), we will nevertheless go to an indirect representation.  We do anticipate supporting packed arrays, but that would initially be handled by doing explicit shifting and masking, rather than by building in the notion of packing into the ParaSail Virtual Machine instruction set.  In the ParaSail Virtual Machine, pretty much everything occupies a single 64-bit word.

So back to the initial question -- how will we represent objects with multiple components (or with a single component whose type is marked optional)?  And how will we represent null for such objects?  One important thing to remember is that (large) ParaSail objects live in regions, and the regions are associated with stack frames.  Whenever assigning a value to an object, if the new value can't "fit" in the same space as its current value, then the space for the old value needs to be released and the space for the new value needs to be allocated, in the appropriate region.  Since a "ref var" parameter (or subcomponent thereof) might be assigned a new value, it won't necessarily be known at compile-time what region the object being assigned "lives" in.  This suggests that every value for a large object must identify its region, so that its space can be released back to that region when it is freed, and so that the new value can be allocated in that region.  This same requirement applies even if the object has a null value to begin with.  Hence, we are left with the conclusion that a null value for a "large" type needs to identify its region.

Another issue for "large" objects is that we need to know how to reclaim the entire "subtree" of subcomponents when we release the enclosing object.  In some cases we will know the type at compile-time, but in the case of polymorphic objects, or in cases where the type of the object is a formal type parameter of the enclosing module, we won't necessarily know.  This implies that we may want to have some kind of "type-id" associated with large objects.  This then results in the following representation for large objects:

    A 64-bit pointer to:
         [Region, Type-Id, component1, component2, component3, ...]

where the Type-Id provides enough information to know which of the components are themselves "large" and hence need to be recursively released.  In addition, there would probably be a special null Type-Id, which would allow the "is null" operation to be implemented relatively efficiently by comparing the Type-Id against some kind of standard "Null-Type-Id" value.  Each region would only need a single null value, which pointed back to the region, and had the Null-Type-Id.  Such null objects would not be reclaimed if they were the "old" value of the left-hand side of an assignment, since there is only one such value per region, and it is shared among all objects in that region currently having a null value.

So to summarize, we now see that null is not a single value, but rather each simple type potentially has its own representation for null, and for "large" types that use a level of indirection, there is a separate null value for each region.  So the "is null" operation is not necessarily a simple check for equality with the global null value, but instead would depend on the type, and in particular for "large" objects, would be a check of the Type-Id field of the object to see if it has the Null-Type-Id.

On a final note, when a function returns "large" values, it needs to be "told" in which region to allocate the value(s) being returned.  One simple way to do this is for the "large" output parameter(s) to be initialized with a (large) null value by the caller.  Since such a null value identifies the region, the function can use that information when allocating the space for the returned value.

Updated YACC grammar for ParaSail

Here is a more up-to-date YACC grammar from ParaSail.  It uses "--" for comments, but otherwise is pretty vanilla "yacc" syntax.

--------------------------------------
-- YACC Grammar for ParaSail
--------------------------------------

-- Single-character delimiters --
%token ',' ';' ':' '.'
%token '+' '-' '*' '/' 
%token '?'
%token '(' ')' '[' ']' '<' '>' ''
%token '|' 
%token '='    -- for error recovery only
%token PRIME -- '''

-- Compound delimiters --
%token COMPARE -- "=?"
%token EQ   -- "=="
%token NEQ  -- "!="
%token GEQ  -- ">="
%token LEQ  -- "<="
%token POWER  -- "**"
%token ASSIGN -- ":="
%token SWAP   -- ":=:"
%token DOT_DOT -- ".."
%token OPEN_CLOSED_INTERVAL -- "<.."
%token OPEN_INTERVAL -- "<..<"
%token CLOSED_OPEN_INTERVAL -- "..<"
%token DOUBLE_COLON  -- "::"
%token REFERS_TO  -- "=>"
%token GIVES    -- "->"
%token IMPLIES    -- "==>"
%token SEQUENCE   -- ";;"
%token PARALLEL   -- "||"
%token PLUS_ASSIGN -- "+="
%token MINUS_ASSIGN -- "-="
%token TIMES_ASSIGN -- "*="
%token DIVIDE_ASSIGN -- "/="
%token POWER_ASSIGN -- "**="
%token CONCAT_ASSIGN -- "|="
%token AND_ASSIGN -- "and="
%token OR_ASSIGN -- "or="
%token XOR_ASSIGN -- "xor="

-- Literals --
%token Char_Literal
%token Enum_Literal
%token Integer_Literal 
%token Real_Literal
%token String_Literal

-- Identifier --
%token Identifier 

-- Reserved words --
%token ABS_kw
%token ABSTRACT_kw
%token ALL_kw
%token AND_kw
%token BEGIN_kw   -- used for error recovery only
%token BLOCK_kw
%token CASE_kw
%token CLASS_kw
%token CONCURRENT_kw
%token CONST_kw
%token CONTINUE_kw
%token EACH_kw
%token ELSE_kw
%token ELSIF_kw
%token END_kw
%token EXIT_kw
%token EXPORTS_kw
%token EXTENDS_kw
%token FOR_kw
%token FORWARD_kw
%token FUNCTION_kw
%token GLOBAL_kw
%token IF_kw
%token IMPLEMENTS_kw
%token IMPORT_kw
%token IN_kw
%token INTERFACE_kw
%token IS_kw
%token LAMBDA_kw
%token LOCKED_kw
%token LOOP_kw
%token MOD_kw
%token MUTABLE_kw
%token NEW_kw
%token NOT_kw
%token NULL_kw
%token OF_kw
%token OPERATOR_kw
%token OPTIONAL_kw
%token OR_kw
%token PRIVATE_kw
%token PROCEDURE_kw
%token QUEUED_kw
%token REF_kw
%token REM_kw
%token RETURN_kw
%token REVERSE_kw
%token SELECT_kw
%token SOME_kw
%token THEN_kw
%token TYPE_kw
%token UNTIL_kw
%token VAR_kw
%token WHILE_kw
%token WITH_kw
%token XOR_kw

%start module_list

%%

module_list : 
    module
  | module_list module
  ;

module : 
    import_clauses interface_declaration ';' 
  | import_clauses class_definition ';' 
  | import_clauses standalone_operation_definition ';'
  | import_clauses error ';'
  ;

import_clauses : 
  | import_clauses IMPORT_kw qualified_name_list ';' 
  ;

qualified_name_list : 
    qualified_name 
  | qualified_name_list ',' qualified_name 
  ;

interface_declaration : 
   opt_interface_qualifier INTERFACE_kw module_defining_name 
     formals_and_implemented_interfaces
     IS_kw
      interface_element_list
   END_kw opt_INTERFACE_kw module_defining_name 
   ; 

opt_INTERFACE_kw : INTERFACE_kw
  | 
  ;
   
opt_interface_qualifier : 
    interface_qualifier 
  | 
  ;

interface_qualifier : 
    class_qualifier 
  | ABSTRACT_kw opt_class_qualifier 
  | PRIVATE_kw opt_class_qualifier 
  ;

opt_class_qualifier : 
    class_qualifier 
  | 
  ;

class_qualifier : CONCURRENT_kw ;

standalone_operation_definition : 
    function_definition 
  | procedure_definition 
  | operator_definition 
  | operation_import 
  ;

formals : '<' opt_module_formal_list '>' ;

formals_and_implemented_interfaces :
    opt_formals opt_implements_list 
  | opt_formals EXTENDS_kw interface_name opt_implements_list 
  ; 

opt_formals : 
    formals  
  | 
  ;

opt_implements_list : 
    implements_list 
  | 
  ;

implements_list : IMPLEMENTS_kw interface_name_list  ;

interface_name_list :
    interface_name 
  | interface_name_list ',' interface_name 
  ;

interface_name : 
    module_name 
  | module_instantiation 
  ;
   
module_name : qualified_name ;

module_defining_name : 
    qualified_name 
  | qualified_name add_on_label 
  ;

add_on_label : 
    '[' operation_actual_list ']' ;

opt_module_formal_list : 
    module_formal_list 
  | ;

module_formal_list : 
    annotated_module_formal 
  | module_formal_list ';' annotated_module_formal 
  ;

annotated_module_formal : 
    opt_annotation type_formal opt_annotation 
  | opt_annotation operation_formal 
  | opt_annotation value_formal opt_annotation 
  ;

opt_annotation : 
    annotation 
  | 
  ;

type_formal : 
    id IS_kw module_instantiation 
  | module_instantiation 
  ;

operation_formal : 
    operation_declaration opt_operation_default  
  ;

opt_operation_default : 
    IS_kw simple_expression 
  | 
  ;

value_formal : 
    id_list ':' opt_output_modifier operand_type_specifier 
  | id_list ':' opt_output_modifier operand_type_specifier 
      ASSIGN_or_equal simple_expression  
  | ref_or_global_modifier operand_type_specifier 
  ;

id : Identifier 
   ;

id_list : 
    id 
  | id_list ',' id 
  ;

type_name : 
    qualified_name 
  | polymorphic_type_name 
  ;

polymorphic_type_name : qualified_name '+' ;

qualified_name : 
    id_or_string_literal 
  | qualified_name DOUBLE_COLON id_or_string_literal ;

id_or_string_literal :
    id 
  | String_Literal 
  ;
  
module_instantiation : 
    module_name '<' opt_module_actual_list '>' 
  | name '[' opt_operation_actual_list ']' '<' opt_module_actual_list '>' 
  ;

opt_add_on_label :
    add_on_label 
  | 
  ;

opt_module_actual_list : 
    module_actual_list 
    | 
    ;

module_actual_list :
    module_actual 
  | module_actual_list ',' module_actual 
  ;

module_actual : 
    simple_type_specifier_or_expression 
  | id REFERS_TO simple_type_specifier_or_expression 
  ;

-- simple_expression subsumes simple type_name in this rule
simple_type_specifier_or_expression : 
    qualified_name annotation 
  | qualified_type_specifier opt_annotation 
  | simple_expression              
    -- simple_expr to avoid problems with '>'
  | lambda_expression 
  | module_instantiation 
  ;
  
annotated_type_specifier : 
    type_specifier 
  | type_specifier annotation 
  ;

type_specifier :
    basic_type_specifier 
  | qualified_type_specifier 
  ;

basic_type_specifier : 
    type_name 
  | module_instantiation 
  | module_instantiation EXTENDS_kw type_specifier 
  ;

qualified_type_specifier : 
    type_qualifier type_name 
  | type_qualifier module_instantiation 
  | type_qualifier module_instantiation 
      EXTENDS_kw type_specifier 
  ;

type_qualifier :
    OPTIONAL_kw opt_MUTABLE_kw opt_CONCURRENT_kw 
  | MUTABLE_kw opt_CONCURRENT_kw 
  | CONCURRENT_kw 
  ;

opt_CONCURRENT_kw : 
    CONCURRENT_kw 
  | 
  ;

interface_element_list : 
  | interface_element_list interface_element ';' 
  | interface_element_list operation_import ';' 
  | interface_element_list error ';' 
  ;

interface_element : 
    operation_declaration 
  | object_declaration 
  | interface_declaration 
  | type_declaration 
  ;

operation_import :
    function_declaration IS_kw import_operation 
  | procedure_declaration IS_kw import_operation 
  | operator_declaration IS_kw import_operation 
  ;

class_definition :
   opt_class_qualifier CLASS_kw module_defining_name 
      class_formals_and_implemented_interfaces
   IS_kw
      class_element_list
   END_kw opt_CLASS_kw module_defining_name ; 

opt_CLASS_kw : CLASS_kw
  | 
  ;
   
class_formals_and_implemented_interfaces :
    formals_and_implemented_interfaces 
  | opt_formals EXTENDS_kw id ':' interface_name opt_implements_list 
  ; 


class_element_list : 
    local_class_element_list
  EXPORTS_kw 
    exported_class_element_list 
  | local_class_element_list
    annotation
  EXPORTS_kw 
    exported_class_element_list 
  | local_class_element_list 
  ;

local_class_element_list : 
  | local_class_element_list local_class_element ';' 
  ;

local_class_element : 
    interface_element  
  | operation_import 
  | annotated_exported_class_element 
  ;
  
exported_class_element_list : 
  | exported_class_element_list annotated_exported_class_element ';' 
  | exported_class_element_list operation_import ';' 
  | exported_class_element_list interface_element ';' 
  | exported_class_element_list error ';' 
  ;

annotated_exported_class_element : 
  | exported_class_element 
  | annotation 
  | annotation exported_class_element 
  ;

exported_class_element : 
    operation_definition  
  | object_definition  
  | class_definition  
  ;
  
   
annotation : '' 
  | annotation '' 
  ;

annotation_element_list : 
    annotation_element 
  | annotation_element_list ';' annotation_element 
  | annotation_element_list ';' error 
  ;

annotation_element : 
    interface_element 
  | operation_import 
  | condition 
  | quantified_expression 
  | annotation 
  ;

condition : expression  ;


operation_declaration : 
    function_declaration 
  | procedure_declaration 
  | operator_declaration 
  ;

function_declaration :
  opt_ABSTRACT_or_OPTIONAL_kw FUNCTION_kw id_or_string_literal
    operation_inputs opt_annotation 
      GIVES_or_RETURN_kw operation_outputs opt_annotation ;

GIVES_or_RETURN_kw : GIVES
  | RETURN_kw 
  ;

procedure_declaration :
  opt_ABSTRACT_or_OPTIONAL_kw PROCEDURE_kw id 
    operation_inputs opt_annotation ;

operator_declaration :
    opt_ABSTRACT_or_OPTIONAL_kw OPERATOR_kw operator_designator 
      operation_inputs opt_annotation 
  | opt_ABSTRACT_or_OPTIONAL_kw OPERATOR_kw operator_designator 
    operation_inputs opt_annotation 
      GIVES_or_RETURN_kw operation_outputs opt_annotation 
  ;

opt_ABSTRACT_or_OPTIONAL_kw :
    ABSTRACT_kw 
  | OPTIONAL_kw 
  | 
  ;

operator_designator : String_Literal ;
  
operation_inputs :
    simple_operation_input 
  | '(' opt_annotated_operation_input_list ')' 
  | '(' id_list ',' id ')' 
  | 
  ;

simple_operation_input :   -- avoids trailing use of "IS"
    id ':' opt_input_modifier simple_operand_type_specifier 
  | input_modifier simple_operand_type_specifier 
  | simple_operand_type_specifier 
  ;

opt_annotated_operation_input_list : 
    annotated_operation_input_list 
  | 
  ;

annotated_operation_input_list : 
    annotated_operation_input 
  | annotated_operation_input_list ';' annotated_operation_input 
  ;

annotated_operation_input : 
    operation_input opt_annotation 
  | annotation operation_input opt_annotation 
  | function_declaration opt_operation_default 
  | annotation function_declaration opt_operation_default 
  | procedure_declaration opt_operation_default 
  | annotation procedure_declaration opt_operation_default 
  ;

operation_input : 
    id_list ':' opt_input_modifier operand_type_specifier opt_ASSIGN_expression
  | input_modifier operand_type_specifier opt_ASSIGN_expression 
  | operand_type_specifier opt_ASSIGN_expression 
  ;

opt_input_modifier : 
    input_modifier 
  | 
  ;
  
simple_operand_type_specifier :
    type_name 
  | module_instantiation 
  ;

operand_type_specifier : 
    simple_operand_type_specifier 
  | id IS_kw module_instantiation 
  ;

input_modifier : 
    output_modifier 
  | QUEUED_kw mutable_or_var_or_const 
  | LOCKED_kw mutable_or_var_or_const 
  ;

mutable_or_var_or_const :
    MUTABLE_kw opt_VAR_kw 
  | VAR_kw 
  | CONST_kw 
  ;

opt_VAR_kw : 
    VAR_kw 
  | 
  ;

operation_outputs : 
    simple_operation_output 
  | annotation simple_operation_output 
  | '(' annotated_operation_output_list ')' 
  | '(' id_list ',' id ')' 
  ;

simple_operation_output :   -- avoids trailing use of "IS"
    id ':' opt_output_modifier simple_operand_type_specifier 
  | output_modifier simple_operand_type_specifier 
  | simple_operand_type_specifier 
  ;

annotated_operation_output_list :
    annotated_operation_output 
  | annotated_operation_output_list ';' annotated_operation_output 
  ;

annotated_operation_output : 
    operation_output opt_annotation 
  | annotation operation_output opt_annotation  
  ;

operation_output : 
  id_list ':' opt_output_modifier operand_type_specifier 
  | output_modifier operand_type_specifier  
  | operand_type_specifier  
  ;

opt_output_modifier :  
    output_modifier 
  | 
  ;

output_modifier :  
    OPTIONAL_kw 
  | ref_or_global_modifier 
  ;

ref_or_global_modifier :
    REF_or_GLOBAL_opt_optional_mutable 
  | REF_or_GLOBAL_opt_optional_mutable VAR_kw 
  | REF_or_GLOBAL_opt_optional_mutable CONST_kw 
  ;

REF_or_GLOBAL_opt_optional_mutable :
    REF_or_GLOBAL_kw 
  | REF_or_GLOBAL_kw OPTIONAL_kw 
  | REF_or_GLOBAL_kw MUTABLE_kw 
  | REF_or_GLOBAL_kw OPTIONAL_kw MUTABLE_kw 
  ;

REF_or_GLOBAL_kw : 
    REF_kw 
  | GLOBAL_kw 
  ;

object_declaration : 
    VAR_kw id ':' 
      annotated_type_specifier 
      opt_ASSIGN_expression 
  | CONST_kw id ':' annotated_type_specifier 
      opt_ASSIGN_expression 
  | id ':' annotated_type_specifier 
      opt_ASSIGN_expression 
  ;

opt_ASSIGN_expression : 
    ASSIGN_or_equal expression 
  | 
  ;
   
object_definition :
    CONST_kw id ASSIGN_or_equal expression 
  | VAR_kw id ASSIGN_or_equal expression 
  | CONST_kw id REFERS_TO name 
  | VAR_kw id REFERS_TO name 
  ;

opt_OPTIONAL_kw : 
    OPTIONAL_kw 
  | 
  ;
opt_MUTABLE_kw : 
    MUTABLE_kw 
  | 
  ;

type_declaration : 
    TYPE_kw id IS_kw opt_NEW_kw annotated_type_specifier ;

opt_NEW_kw : 
    NEW_kw 
  | 
  ;

operation_definition : 
    function_definition 
  | procedure_definition 
  | operator_definition 
  ;

function_definition : 
  function_declaration IS_kw opt_queued_clause 
     statement_list_with_semi 
  END_kw opt_FUNCTION_kw id 
  ;

opt_FUNCTION_kw : FUNCTION_kw
  | 
  ;

procedure_definition : 
  procedure_declaration IS_kw opt_queued_clause 
     statement_list_with_semi 
  END_kw opt_PROCEDURE_kw id 
  ;

opt_PROCEDURE_kw : PROCEDURE_kw
  | 
  ;

operator_definition : 
  operator_declaration IS_kw 
     statement_list_with_semi 
  END_kw opt_OPERATOR_kw operator_designator  
  ;

opt_OPERATOR_kw : OPERATOR_kw
  | 
  ;

opt_queued_clause : 
    queued_clause 
  | 
  ;

queued_clause :
    QUEUED_kw WHILE_or_UNTIL_kw condition THEN_kw ;

import_operation :
    IMPORT_kw '(' opt_operation_actual_list ')' ;

statement_list_with_semi : 
    parallel_sequence_with_semi 
  | statement_list_no_semi THEN_kw parallel_sequence_with_semi 
  | statement_list_with_semi THEN_kw parallel_sequence_with_semi 
  | statement_list_with_semi use_BEGIN_kw parallel_sequence_with_semi 
  | use_BEGIN_kw parallel_sequence_with_semi 
  ;

use_BEGIN_kw : BEGIN_kw ;


statement_list_no_semi : 
    parallel_sequence_no_semi 
  | statement_list_no_semi THEN_kw parallel_sequence_no_semi 
  | statement_list_with_semi THEN_kw parallel_sequence_no_semi 
  ;

parallel_sequence_with_semi : 
    statement_sequence_with_semi 
  | parallel_sequence_no_semi PARALLEL statement_sequence_with_semi 
  | parallel_sequence_with_semi PARALLEL statement_sequence_with_semi 
  ;

parallel_sequence_no_semi :
    statement_sequence 
  | parallel_sequence_no_semi PARALLEL statement_sequence 
  | parallel_sequence_with_semi PARALLEL statement_sequence 
  ;

statement_sequence_opt_semi :
    statement_sequence_with_semi 
  | statement_sequence 
  ;

statement_sequence_with_semi : statement_sequence ';' ;

statement_sequence :
    annotated_statement 
  | statement_sequence SEQUENCE annotated_statement 
  | statement_sequence ';' SEQUENCE annotated_statement 
  | statement_sequence ';' annotated_statement 
  ;
  
annotated_statement : 
    opt_annotation local_declaration 
  | opt_annotation statement opt_annotation 
  | annotation 
  ;

statement : 
    local_definition 
  | simple_statement 
  | label compound_statement 
  | compound_statement 
  ;

simple_statement :
    primitive_statement 
  | name equal_as_assign expression 
  | NULL_kw 
  | name '(' opt_operation_actual_list ')' 
  | RETURN_kw expression 
  | RETURN_kw opt_WITH_values  
  | CONTINUE_kw LOOP_kw opt_id opt_WITH_values  
  | EXIT_kw compound_statement_kind opt_id opt_WITH_values 
  ;

primitive_statement :
    name assign_operator_not_divide expression 
  | name DIVIDE_ASSIGN expression 
  | name SWAP name 
  | '(' opt_operation_actual_list ')' ASSIGN expression 
  ;

opt_operation_actual_list : 
    operation_actual_list 
  | 
  ;

opt_WITH_values : 
    WITH_values 
  | 
  ;

WITH_values : WITH_kw operation_actual ;

opt_id : 
    id 
  | 
  ;

compound_statement_kind : 
    LOOP_kw 
  | IF_kw 
  | CASE_kw 
  | SELECT_kw 
  | BLOCK_kw 
  ;

local_declaration : 
    operation_declaration 
  | type_declaration 
  | object_declaration
  ;

local_definition :
    object_definition 
  | operation_definition 
  ;

label : '*' id '*' ;

compound_statement :
    if_statement 
  | case_statement 
  | indefinite_loop_statement 
  | while_until_loop_statement 
  | for_loop_statement 
  | block_statement  
  | select_statement 
  | error ';' 
  ;

if_statement : 
  IF_kw condition THEN_kw 
     statement_list_with_semi
  opt_else_part
  END_kw IF_kw opt_id opt_WITH_values ;

opt_else_part : 
    ELSIF_kw condition THEN_kw
      statement_list_with_semi 
    opt_else_part 
  | ELSE_kw statement_list_with_semi 
  | 
  ;


case_statement : 
  CASE_kw expression OF_kw
    case_alt_list
    opt_default_alt
  END_kw CASE_kw opt_id opt_WITH_values ;

case_alt_list : 
    case_alt 
  | case_alt_list case_alt 
  ;

case_alt :
    '[' simple_expression_opt_named ']' REFERS_TO statement_list_with_semi 
  ;

simple_expression_opt_named :
    simple_expression 
  | id ':' simple_expression 
  ;
  
opt_default_alt : 
    '[' dot_dot_opt_named ']' REFERS_TO statement_list_with_semi 
  | 
  ;

dot_dot_opt_named :
    dot_dot_as_interval 
  | id ':' dot_dot_as_interval 
  ;
    
dot_dot_as_interval : DOT_DOT ;


indefinite_loop_statement :
  LOOP_kw 
    statement_list_with_semi
  END_kw LOOP_kw opt_id opt_WITH_values ;

while_until_loop_statement :
  WHILE_or_UNTIL_kw condition LOOP_kw
    statement_list_with_semi
  END_kw LOOP_kw opt_id opt_WITH_values ;

WHILE_or_UNTIL_kw :
    WHILE_kw 
  | UNTIL_kw 
  ;

for_loop_statement :
  FOR_kw iterator_spec opt_direction LOOP_kw
    statement_list_with_semi
  END_kw LOOP_kw opt_id opt_WITH_values ;

iterator_spec : 
    iterator 
  | '(' iterator_list ')' 
  ;

iterator_list :
    iterator 
  | iterator_list ';' iterator 
  ;

iterator :
    index_set_iterator 
  | EACH_kw element_iterator 
  | initial_next_while_iterator 
  | initial_value_iterator 
  ;

index_set_iterator :
    id opt_COLON_type_specifier IN_kw opt_REVERSE_kw expression ;

opt_REVERSE_kw : 
  | REVERSE_kw ;

element_iterator :
    id opt_COLON_type_specifier OF_kw expression 
  | '[' id REFERS_TO id ']' OF_kw expression 
  ;

initial_next_while_iterator :
    id opt_COLON_type_specifier ASSIGN_or_equal expression 
      opt_THEN_next_value_list 
      WHILE_or_UNTIL_kw condition 
  | id opt_COLON_type_specifier REFERS_TO name 
      opt_THEN_next_name_list
      WHILE_or_UNTIL_kw condition 
  ;

opt_THEN_next_value_list :
    THEN_kw next_value_list 
  | 
  ;

opt_THEN_next_name_list :
    THEN_kw next_name_list 
  | 
  ;

initial_value_iterator :
    id opt_COLON_type_specifier ASSIGN_or_equal expression 
  | id opt_COLON_type_specifier REFERS_TO name 
  ;

opt_COLON_type_specifier : 
    ':' type_specifier 
  | 
  ;

next_value_list : 
    expression  
  | next_value_list PARALLEL expression 
  ;

next_name_list : 
    name  
  | next_name_list PARALLEL name 
  ;

opt_direction : direction  
  | 
  ;

direction : 
    CONCURRENT_kw 
  | FORWARD_kw 
  | REVERSE_kw 
  ;

select_statement :
  SELECT_kw 
     select_alt_list
  END_kw SELECT_kw opt_id opt_WITH_values ;

select_alt_list : 
    select_alt
  | select_alt_list PARALLEL select_alt
  ;

select_alt : 
  '[' statement_sequence_opt_semi ']' REFERS_TO statement_sequence_with_semi ;

block_statement :
    BLOCK_kw
      statement_list_with_semi
    END_kw opt_BLOCK_kw opt_id opt_WITH_values 
  ;

opt_BLOCK_kw : BLOCK_kw
  | 
  ;
   
expression :
    expression_no_err 
  | expression_no_err divide_assign_as_not_equal expression_no_err 
  ;

divide_assign_as_not_equal :
    DIVIDE_ASSIGN 
  ;

expression_no_err :
    logical_expression 
  | logical_expression '?' expression ':' expression_no_err 
  | lambda_expression 
  ;

lambda_expression :
    LAMBDA_kw operation_inputs opt_annotation IS_kw 
       simple_expression_or_expr_stmt_seq 
  | LAMBDA_kw operation_inputs opt_annotation
      GIVES operation_outputs opt_annotation IS_kw 
    simple_expression_or_expr_stmt_seq 
  ;

simple_expression_or_expr_stmt_seq :
    simple_expression 
  | '(' expr_statement_seq ')' 
  ;

expr_statement_seq : expr_statement ';' expr_statement 
  | expr_statement_seq ';' expr_statement 
  ;

expr_statement : 
    primitive_statement 
  | expression_no_err 
  ;

logical_expression :  
    comparison_expression 
  | logical_expression logical_operator comparison_expression 
  ;

comparison_expression :  -- comparisons are non associative
    simple_expression 
  | simple_expression comparison_operator simple_expression 
  | adding_expression IN_kw simple_expression 
  | adding_expression NOT_kw IN_kw simple_expression 
  | adding_expression IS_kw NULL_kw 
  | adding_expression NOT_kw NULL_kw 
  ;

simple_expression : -- used to avoid use of '>' in module instantiation
    simple_expression_component 
  | simple_expression '|' simple_expression_component 
  ;

simple_expression_component :
    adding_expression 
  | adding_expression interval_operator adding_expression 
  | adding_expression interval_operator 
  | interval_operator adding_expression 
  | adding_expression '+' 
  ;

adding_expression :
    term 
  | adding_expression adding_operator term 
  ;

term : 
    factor 
  | term multiplying_operator factor 
  ;

factor : 
    primary 
  | primary power_operator factor 
  | unary_operator factor  
  ;

primary :
    name 
  | literal 
  | '(' conditional_expression ')' 
  | '(' quantified_expression ')' 
  | aggregate 
  ;
  
literal:  -- NOTE: See "name" for String_Literal
    Integer_Literal 
  | Real_Literal 
  | Char_Literal 
  | Enum_Literal 
  | NULL_kw 
  ;

name :
    qualified_name_and_property opt_PRIME 
  | qualified_name DOUBLE_COLON literal 
  | name '(' opt_operation_actual_list ')' 
  | name '[' opt_operation_actual_list ']' 
  | name '.' selector 
  ;

qualified_name_and_property :
    qualified_name 
  | qualified_name_and_property Enum_Literal 
  ;

opt_PRIME : 
    PRIME 
  | PRIME Identifier 
  | 
  ;

operation_actual_list : 
    operation_actual 
  | operation_actual_list ',' operation_actual 
  ;

operation_actual : 
    expression_no_err 
  | id REFERS_TO expression 
  ;

selector : id ;

unary_operator : 
    '+' 
  | '-' 
  | ABS_kw 
  | NOT_kw 
  ;

adding_operator : 
  '+' 
  | '-' 
  ;

multiplying_operator : 
    '*' 
  | '/' 
  | MOD_kw 
  | REM_kw 
  ;

power_operator : POWER ;

assign_operator : assign_operator_not_divide 
  | DIVIDE_ASSIGN 
  ;

assign_operator_not_divide :
    ASSIGN 
  | PLUS_ASSIGN 
  | MINUS_ASSIGN 
  | TIMES_ASSIGN 
  | CONCAT_ASSIGN 
  | AND_ASSIGN 
  | OR_ASSIGN 
  | XOR_ASSIGN 
  ;

ASSIGN_or_equal : ASSIGN 
  | equal_as_assign 
  ;

equal_as_assign : '=' 
  ;

comparison_operator : 
    COMPARE 
  | EQ 
  | NEQ 
  | '<' 
  | LEQ 
  | '>' 
  | GEQ 
  | '<' '<' 
  | '>' '>' 
  | '=' 
  ;

logical_operator :
    AND_kw 
  | OR_kw 
  | XOR_kw  
  | AND_kw THEN_kw 
  | OR_kw ELSE_kw 
  | IMPLIES 
  ;

interval_operator :
    DOT_DOT 
  | OPEN_INTERVAL 
  | CLOSED_OPEN_INTERVAL 
  | OPEN_CLOSED_INTERVAL 
  ;

aggregate : 
    class_aggregate  
  | container_aggregate  
  ;

class_aggregate : 
    '(' opt_operation_actual_list ')' 
  | '(' name DIVIDE_ASSIGN expression ')' 
  | qualified_name DOUBLE_COLON '(' opt_operation_actual_list ')' 
  ;

container_aggregate : 
    '[' opt_container_element_list ']' 
  | qualified_name DOUBLE_COLON '[' opt_container_element_list ']' 
  ;
  
opt_container_element_list : 
    container_element_list 
  | DOT_DOT 
  | 
  ;

container_element_list : 
    container_element 
  | container_element_list ',' container_element 
  ;

container_element : 
    expression 
  | simple_expression REFERS_TO filtered_expression_stream 
  | DOT_DOT REFERS_TO filtered_expression_stream 
  | FOR_kw iterator REFERS_TO filtered_expression_stream 
  ;

filtered_expression_stream : 
    expression 
  | expression ':' condition 
  ;

conditional_expression :
    if_expression 
  | case_expression 
  ;

if_expression : 
  IF_kw condition THEN_kw 
     expression
  opt_else_expr ;

opt_else_expr : 
    ELSIF_kw condition THEN_kw 
      expression 
    opt_else_expr 
  | ELSE_kw expression 
  | 
  ;

case_expression : 
  CASE_kw expression OF_kw
    case_expr_alt_list ;

case_expr_alt_list : 
    case_expr_alt 
  | case_expr_alt_list ';' case_expr_alt 
  ;

case_expr_alt : 
    '[' simple_expression_opt_named ']' REFERS_TO expression 
  | '[' dot_dot_opt_named ']' REFERS_TO expression 
  ;

quantified_expression :
    FOR_kw ALL_or_SOME_kw quantified_iterator REFERS_TO
      condition_or_quantified_expression ;

condition_or_quantified_expression :
    condition 
  | if_expression 
  | quantified_expression 
  ;

ALL_or_SOME_kw : 
    ALL_kw 
  | SOME_kw 
  ;

quantified_iterator :
    index_set_iterator 
  | element_iterator 
  | initial_next_while_iterator 
  ;

%%

ParaSail Reference Manual -- first complete draft posted

We have posted the first complete draft of the reference manual for the ParaSail programming language to the ParaSail google group:

  http://groups.google.com/group/parasail-programming-language

Comments welcomed!

Writing preconditions and postconditions incrementally

Once you start enforcing pre- and postconditions at compile time, as in ParaSail, some interesting things start to happen.  Unless programmers are very familiar with writing pre- and postconditions as a matter of course, chances are that the code will be written initially with few if any pre/postconditions.  However, presuming that the language-provided abstractions, such as Arrays, already have some preconditions (such as you cannot index into an array with an index that is out of the array bounds), the compiler pretty quickly identifies places where the programmer will have to write some of their own preconditions, constraints, invariants, etc.  For example, consider the classic Stack abstraction.  This might be written in ParaSail as follows, initially without any pre/postconditions:

interface Stack
  <Component is Assignable<>; 
   Size_Type is Integer<>> is
    function Create(Max : Size_Type) -> Stack;
    function Top(S : ref Stack) -> ref Component;
    procedure Pop(S : ref var Stack);
    procedure Push
      (S : ref var Stack; 
       X : Component);     
end interface Stack;

class Stack is
    const Max_Len : Size_Type;
    var Cur_Len : Size_Type;
    type Index_Type is Size_Type {Index_Type in 1..Max_Len};
    var Data : Array<optional Component, Indexed_By => Index_Type>;    
  exports
    function Create(Max : Size_Type) -> Stack is
      return (Max_Len => Max, Cur_Len => 0, Data => [.. => null]);
    end function Create;

    procedure Push(S : ref var Stack; X : Component) is
      S.Cur_Len += 1;
      S.Data[S.Cur_Len] := X;
    end procedure Push;
      
    function Top(S : ref Stack) -> ref Component is
      return S.Data[S.Cur_Len];
    end function Top;                

    procedure Pop(S : ref var Stack) is
      S.Cur_Len -= 1;
    end procedure Pop;     
end class Stack;

This all looks pretty straightforward until we try to compile it, and the compiler begins to complain at various places. For example, we blithely add one to S.Cur_Len in Push without any apparent concern about overflow. Then we blithely use the incremented S.Cur_Len as an index into S.Data, again with no apparent concern for the index being out of bounds.

The ParaSail compiler is never blithe, and will complain because the Array abstraction imposes a precondition on the indexing into S.Data, requiring that the index be in the range of Index_Type (1..Max_Len). It will also complain because the increment of S.Cur_Len might cause it to exceed the maximum Size_Type value (this precondition is from the "+=" operation of the Integer abstraction).

We could resolve these problems by adding a meaningful constraint on the range of values of Cur_Len (namely {Cur_Len in 0 .. Max_Len}) and adding a precondition on the Push operation ensuring that Cur_Len < Max_Len before any call on Push.  However, Cur_Len and Max_Len are not exported in the Stack interface, so we need to provide functions that reveal their value, say "Count" and "Max_Stack_Size."  So our new Stack abstraction would look like this:

interface Stack
  <Component is Assignable<>; 
   Size_Type is Integer<>> is
    function Max_Stack_Size(S : Stack) -> Size_Type;
    function Count(S : Stack) -> Size_Type;
    function Create(Max : Size_Type) -> Stack;
    function Top(S : ref Stack) -> ref Component;
    procedure Pop(S : ref var Stack);
    procedure Push
      (S : ref var Stack {Count(S) < Max_Stack_Size(S)}; 
       X : Component);
end interface Stack;

class Stack is
    const Max_Len : Size_Type;
    var Cur_Len : Size_Type {Cur_Len in 0..Max_Len};
    type Index_Type is Size_Type {Index_Type in 1..Max_Len};
    var Data : Array<optional Component, Indexed_By => Index_Type>;    
  exports
    function Max_Stack_Size(S : Stack) -> Size_Type is
      return S.Max_Len;
    end function Max_Stack_Size;
    
    function Count(S : Stack) -> Size_Type is
      return S.Cur_Len;
    end function Count; 

    function Create(Max : Size_Type {Max > 0}) -> Stack is
      return (Max_Len => Max, Cur_Len => 0, Data => [.. => null]);
    end function Create;

    procedure Push
      (S : ref var Stack {Count(S) < Max_Stack_Size(S)}; 
       X : Component) is
      S.Cur_Len += 1;
      S.Data[S.Cur_Len] := X;
    end procedure Push;
      
    function Top(S : ref Stack) -> ref Component is
      return S.Data[S.Cur_Len];
    end function Top;                

    procedure Pop(S : ref var Stack) is
      S.Cur_Len -= 1;
    end procedure Pop;
end class Stack;

So with these changes, Push should now compile. However, we are going to run into similar problems in Top and Pop, and we will need a precondition on both of those of {Count(S) > 0}.  Top also presents a more subtle problem.  The Data array is defined as being an array of optional Element_Type, but we are returning S.Data[S.Cur_Len] with a return type of simply Element_Type, implying that we somehow know that S.Data[S.Cur_Len] is not null.  So how do we know that?  Well, we know that Push only pushes non-null elements onto the stack (because the parameter type for X is a non-optional Element_Type.  But Data starts out all null, and when looking only at Top we have no way of knowing that S.Data[S.Cur_Len] is not null.

What we need is some kind of class invariant which ensures that when we get into Top, S.Data[S.Cur_Len] is not null.  What might that invariant look like?  What we know about a stack is that all of the elements that have been pushed onto the stack are non-null, but the slots in the stack past Cur_Len might be null if they have never been used.  So our invariant would seem to be:

   {for all I in 1..Cur_Len => Data[I] not null}

The basic requirement for a class invariant is that, presuming it is true on entering any externally visible operation, it is true again on exiting that operation.  It might be false in the middle of some operation, but it is preserved overall by all visible operations.  Furthermore, for any operation that creates an object of type Stack, the returned object must satisfy the invariant.

So let us check whether the above proposed invariant is true upon creation of a Stack object, and is preserved by operations that modify a Stack.  Create produces a new value with Cur_Len == 0, so the invariant is trivially true, since there are no values in the interval 1..Cur_Len.  Push and Pop modify a Stack object.  Pop is trivial since it is decrementing Cur_Len, so the interval 1..Cur_Len is shrinking.  Push is not trivial, because it is adding one to Cur_Len.  But if we presume the invariant holds on entry to Push, then the only new value to worry about is S'.Data[S'.Cur_Len], where S' represents the value of S after the Push operation is complete.  Since S'.Data[S'.Cur_Len] is set to X, and X is not null, our invariant is preserved.

Note that we might have tried an invariant of simply {Data[Cur_Len] not null}, which would have satisfied Top, and would be preserved by Push, but it would not be preserved by Pop, since without the more sophisticated invariant, Pop would know nothing about S'.Data[S'.Cur_Len].  It might be null if the invariant only claims that the very top element is non-null.

So after adding the class invariant, and the various preconditions, we can now get the Stack abstraction to compile.  However, it now becomes time to write some code that tests the Stack abstraction.  What we quickly discover is that the compiler rejects any call on any Stack operation with a precondition, since there are no postconditions that would allow it to know whether Count(S) > 0 or Count(S) < Max_Stack_Size(S).  At the call site there is no peeking into the class that defines the interface.  The compiler must prove the preconditions of the call looking only at information in the interface.  And without any postconditions, the compiler is stuck.

So now we have to start adding postconditions to the operations.  If we do a Create and then immediately try to do a Push onto the created stack object, our first job is to prove that Count(S) < Max_Stack_Size(S).  This implies we need a postcondition on Create that indicates the values of Count() and Max_Stack_Size() for the result of Create.  We could write this as follows:

   {Max_Stack_Size(Create) == Max; Count(Create) == 0} 

What this says is that the result of Create (within a postcondition, we can use the name of the creating function to represent the result) has a Max_Stack_Size that corresponds to the passed in parameter Max, and starts out with a Count of zero.  No big surprise here, but without such a postcondition the compiler would be pretty much at a loss.  We also might want to impose a precondition on Max of {Max > 0} just so the stack is at least of some use.

Next question we might have is what happens to Count as a result of Push.  This brings up an interesting question that is sometimes called the frame problem.  How do we know what might be written by an operation -- what is the write frame?  (We might also be interested in exactly what might be read by an operation -- what is the read frame -- but that is less relevant as far as checking preconditions.)  Since the Push operation has S as a ref var parameter, we could assume the worst and assume any function of S' (the value of S after Push) might return a different value, so after Push we know pretty much nothing about Count(S') and Max_Stack_Size(S').  Alternatively, we could take the view that if there is no postcondition, then nothing is changed. 

For ParaSail we are (tentatively) adopting a model that for any function of S mentioned in any precondition of an operation on a Stack object S, if such a function is not mentioned in a postcondition then it is presumed unchanged.  Now that we have mentioned Count() and Max_Stack_Size() in the preconditions of Push, we are duty bound to write postconditions any time the value of Count() or Max_Stack_Size() is changed.  This obligation will be checked when we compile the Stack class, so having written some preconditions, the compiler is going to start complaining because Count(S') is clearly going to be different from Count(S) after the call on Push.  Similar obligations will apply to Pop.  So now we will need to add a postcondition to Push of {Count(S') == Count(S) + 1} and a postcondition to Pop of {Count(S') == Count(S) - 1}.  We don't need to say that {Max_Stack_Size(S') == Max_Stack_Size(S)} because as indicated, our default assumption is that anything used in any precondition, but not mentioned in a postcondition, is presumed to be unchanged by the operation.  Again, the compiler will check that when it compiles the code for the operation.  If we don't want to say anything about the new value other than it is not the same as the old value, we could say {Some_Property(S') != Some_Property(S)}.  That won't help the compiler with proving later preconditions, but it will at least satisfy the obligation to mention the changed property in a postcondition.

So if we continue this process until we make the compiler happy, both with the Stack module itself, and with our various test programs, we will probably end up with a relatively fully annotated Stack like the following:

interface Stack
  <Component is Assignable<>; 
   Size_Type is Integer<>> is
    function Max_Stack_Size(S : Stack) -> Size_Type;
    function Count(S : Stack) -> Size_Type;

    function Create(Max : Size_Type {Max > 0}) -> Stack 
      {Max_Stack_Size(Create) == Max; Count(Create) == 0};
    
    procedure Push
      (S : ref var Stack {Count(S) < Max_Stack_Size(S)}; 
       X : Component) {Count(S') == Count(S) + 1};

    function Top(S : ref Stack {Count(S) > 0}) -> ref Component;
    
    procedure Pop(S : ref var Stack {Count(S) > 0}) 
      {Count(S') == Count(S) - 1};
end interface Stack;

class Stack is
    const Max_Len : Size_Type;
    var Cur_Len : Size_Type {Cur_Len in 0..Max_Len};
    type Index_Type is Size_Type {Index_Type in 1..Max_Len};
    var Data : Array<optional Component, Indexed_By => Index_Type>;    
  exports
    {for all I in 1..Cur_Len => Data[I] not null}   // invariant for Top()

    function Max_Stack_Size(S : Stack) -> Size_Type is
        return S.Max_Len;
    end function Max_Stack_Size;
    
    function Count(S : Stack) -> Size_Type is
      return S.Cur_Len;
    end function Count; 

    function Create(Max : Size_Type {Max > 0}) -> Stack
      {Max_Stack_Size(Create) == Max; Count(Create) == 0} is
      return (Max_Len => Max, Cur_Len => 0, Data => [.. => null]);
    end function Create;

    procedure Push
      (S : ref var Stack {Count(S) < Max_Stack_Size(S)}; 
       X : Component) {Count(S') == Count(S) + 1} is
      S.Cur_Len += 1;
      S.Data[S.Cur_Len] := X;
    end procedure Push;
      
    function Top(S : ref Stack {Count(S) > 0}) -> ref Component is
      return S.Data[S.Cur_Len];
    end function Top;                

    procedure Pop(S : ref var Stack {Count(S) > 0}) 
      {Count(S') == Count(S) - 1} is
        S.Cur_Len -= 1;
    end procedure Pop;
end class Stack;

One thing to note is that the compiler has not forced us to create postconditions that ensure all the nice properties of Stacks, such as after Push(S,X), then Top(S') == X, or if Top(S) == A, then after Push(S, X) and Pop(S'), Top(S'') == A.  These might be called correctness preconditions as opposed to merely safety preconditions, and they are up to the programmer to add if they see fit.  We have considered having a second class annotation in ParaSail which is not required to be provable at compile-time, but is designed to aid in correctness proofs, and provide additional debugging support.  We have set aside a syntax of doubly nested {{...}} for such correctness preconditions, but we aren't worrying about them more than that at this point.

WoDet 2011, ParaSail, and back to the future with Value Semantics

This past Sunday WoDet 2011, the 2nd Workshop on Determinism and Correctness in Parallel Programming was held in Newport Beach, CA.  It was a very interesting event, with a number of excellent talks and a lively debate at the end on the topic of whether current programming models are sufficient given the right tools, etc., or whether we need fundamentally new models to support programming going forward in a multi-core world. 

After listening to the various talks at the workshop, and while thinking about the debate topic, it seemed that ParaSail aligned nicely with an underlying thread in the research community moving toward, or perhaps returning to, what might best be called value semantics.  A number of the talks described one variant or another of multi-version concurrency control, which at its heart involves giving different threads their own private copy/version/snapshot of an object, and then dealing with merging any updates at specific later points, possibly rolling back one of the threads if no meaningful merge is possible.  This is in contrast to an approach where multiple threads share access to a single object, and use some kind of locking or "careful" lock-free operations to make direct updates to the shared object.  The multi-version approach results in fewer interactions between the threads, fewer synchronization points, and hence generally higher throughput in a highly parallel world. 

Looked at another way, the multi-version approach means that objects are being passed around by value rather than by reference, and updating the original object is done after all the new "values" have been generated independently and then appropriately merged (perhaps using some kind of parallel merging process).  This isn't going all the way to pure functional programming, because updates can eventually happen, but the bulk of the processing is performed on object values, with no underlying sharing.

If we go all the way back to the original versions of BASIC, a la Kemeny and Kurtz or Microsoft CP/M BASIC, pointers didn't exist, but there were strings, and you could create them and concatenate them and assign them, and you never by mistake overwrote memory because you concatenated into a too-short buffer, nor did you ever have two variables unintentionally referring to the "same" string in memory, such that changing one would unintentionally alter what you had in the other (even though the implementation might choose to share the space until one of them was altered). 

These kinds of value-semantics strings still exist in many scripting languages, but they have essentially disappeared from compiled languages in the years since BASIC was widely used (and compiled, in some cases).  In almost all modern compiled languages, strings are manipulated by reference, though in some languages they are immutable which to some extent skirts the issue of by-value vs. by-reference semantics.  And certainly when you get to larger, more abstract objects, by-reference semantics rules, with only the simplest of "struct" objects being manipulated by value.  And even when declared objects have value semantics, parameters generally revert to by-reference semantics, again introducing the possibility of unintended aliasing between two distinctly named objects.  (Or if by-value semantics are available for parameter passing (as in C++), it can result in "slicing" of the object, so that it is truncated from its original run-time type to the compile-time type of the formal parameter.)

Unintended aliasing due to by-reference semantics can cause nasty (but still reproducible) bugs in any sequential language that uses by-reference semantics, but in a parallel language, such bugs can become race conditions, which can result in hard-to-reproduce, timing-dependent bugs.

In any case, the net effect of the various ParaSail rules that restrict aliasing, eliminate reassignable pointers, disallow global variables, etc. is that ParaSail provides value semantics for all non-concurrent objects, of arbitrarily complex types.  Note that this does not imply that objects need to be copied when passed as a parameter.  Rather the ParaSail rules allow non-concurrent objects to be passed by reference or by copy, with the same results. This allows efficient by-reference parameter passing when the call stays within the same address space, but allows transferring the object between address spaces, such as might be needed by a call between a CPU and a GPU.  This essentially value semantics eliminates a large class of common bugs, and makes it straightforward for the compiler to detect and disallow at compile-time any possible race conditions.

As implied by the growing interest in multi-version concurrency control in the research community, a return to the world of value semantics might be a good answer for the multi-core challenges.

Streaming in Parasail -- A Unix-like pipeline

We have been considering how streaming can best be supported in ParaSail.  By streaming we mean having a series of components each of which reads inputs from a stream and writes outputs to a stream, with each component running in parallel with the others.  The most natural seems to be to define an abstract Stream_Component interface which takes an Input_Stream and Output_Stream type and declares an operation Transform which reads one or more input elements from the Input_Stream, transforms the input(s) in some way, and then writes one or more output elements to the Output_Stream.   An actual component would be defined by some concrete module that implements this abstract interface, with an appropriate constructor function that provides whatever arguments are needed to specify or control the transformation.

This might be the abstract Stream_Component interface:

abstract interface Stream_Component
  <Input_Stream<>; Output_Stream<>> is
    procedure Transform
      (Args : Stream_Component;
       Inp : ref var Input_Stream; 
       Outp : ref var Output_Stream);
end interface Stream_Component;

The Input_Stream and Output_Stream interfaces might look like this:

abstract concurrent interface Input_Stream
  <Element_Type is Assignable<>> is
    function Get(Stream : queued var Input_Stream) -> optional Element_Type;
end interface Input_Stream;

abstract concurrent interface Output_Stream
  <Element_Type is Assignable<>> is
    procedure Put
      (Stream : queued var Output_Stream; Element : Element_Type);
    procedure Close(Stream : queued var Output_Stream);
end interface Output_Stream;

We now want to put together two or more stream components into a pipeline. Let us presume we define a Pipeline interface:

interface Pipeline
  <Pipe_Input is Input_Stream<>;
   Pipe_Output is Output_Stream<>> 
  implements Stream_Component<Pipe_Input, Pipe_Output> is
    operator "|"
     (Left is Stream_Component
        <Pipe_Input,
         Output_Stream<Internal_Type is Assignable<>>;
      Right is Stream_Component
        <Input_Stream<Internal_Type>,
         Pipe_Output>)
     -> Pipeline;
    procedure Transform
      (Args : Pipeline;
       Inp : ref var Pipe_Input; 
       Outp : ref var Pipe_Output);
end interface Pipeline;

The pipeline "|" operator takes two stream components and produces a Pipeline stream component, feeding the output of the first stream component into the input for the second stream component, by using an IO_Queue:

concurrent interface IO_Queue<Element_Type is Assignable<>> 
  implements Input_Stream<Element_Type>, Output_Stream<Element_Type> is
    function Create(Buffer_Size : Univ_Integer := 100) -> IO_Queue;
    function Get(Queue : queued var IO_Queue) -> optional Element_Type;
    procedure Put
      (Queue : queued var IO_Queue; Element : Element_Type);
    procedure Close(Queue : queued var IO_Queue);
end interface IO_Queue;

When constructing a pipeline from two stream components, the output stream of the first must have the same Element_Type as the input stream for the second, so that they can be opposite ends of the IO_Queue. The result pipeline has the same input stream as the first, and the same output stream as the second. The implementation of the pipeline Transform procedure would construct an IO_Queue object and then pass it to parallel invocations of the Transform procedures of the two stream components:

class Pipeline is
    const Left : Stream_Component+;
    const Right : Stream_Component+;
  exports
    operator "|"
     (Left is Stream_Component
        <Pipe_Input,
         Output_Stream<Internal_Type is Assignable<>>;
      Right is Stream_Component
        <Input_Stream<Internal_Type>,
         Pipe_Output>)
     -> Pipeline is
      return (Left => Left; Right => Right);
    end operator "|"; 
    procedure Transform
      (Args : Pipeline;
       Inp : ref var Pipe_Input; 
       Outp : ref var Pipe_Output) is
        var Queue : IO_Queue := Create();
      then
        Transform(Left, Inp, Queue);
      || 
        Transform(Right, Queue, Outp);
    end procedure Transform;
end class Pipeline;

If we have a set of components with both input and output streams being streams of characters, then the "|" operator is essentially equivalent to the Unix shell's "|" pipe command. To write a "program" that is compatible with such a pipeline, we define a module that implements Stream_Component, with Input_Stream and Output_Stream both having Element_Type of Character<>. Any constructor function within such a module may be used to provide the parameters to the program. The Transform procedure of the module is the one that actually performs the action of the program. Alternatively, we can be somewhat more flexible, and allow the streams to have higher level element types, such as words or lines.

For example, here is a trivial "element count" program, which allows the input element type to be any sort of thing. The output element type is presumed to be some Character type:

interface Elem_Count
  <Input_Stream<>, Output_Stream<Character<>>>
  implements Stream_Component
    <Input_Stream, Output_Stream> is
    function Args()->Elem_Count;  // takes no parameters
    procedure Transform
      (Args : Elem_Count;
       Inp : ref var Input_Stream; Outp : ref var Output_Stream);
       // Prints a count of the elements in Inp on the Outp stream
end interface Elem_Count;

class Elem_Count is
  exports
    function Args() -> Result : Elem_Count is
      return;
    end function Args;
    procedure Transform
      (Args : Character_Count;
       Inp : ref var Input_Stream; Outp : ref var Output_Stream) is
       // Prints a count of the elements in Inp on the Outp stream
       var Count : Univ_Integer := 0;
       while Get(Inp) not null loop
         Count += 1;
       end loop;
       const Answer : String<Output_Stream::Element_Type> := To_String(Count);
       // Copy the answer to the output stream one character at a time
       // (in all probability, we would actually use an output stream
       //  with an operation that takes a string of characters directly).
       for each C of Answer forward loop
          Put(Outp, C);
       end loop;
       Close(Outp);
    end procedure Transform;
end class Elem_Count; 

In a more realistic example, the Args constructor function would take one or more arguments, which it would store as fields of the stream component object. The Transform procedure would refer to the arguments using the Args parameter, which is an instance of the stream component object.

Presuming we create a number of stream components like Elem_Count, we could construct a pipeline like the following:

Read::Args("my_file.txt") | Break_Into_Words::Args() | Elem_Count::Args()

This would presumably read my_file.txt producing a stream of characters, break it into a stream of words, and then count the words and produce the count as a string on the output stream of characters. With a little syntactic sugar by some kind of ParaSail "shell" this could become:

Read my_file.txt | Break_Into_Words | Elem_Count

This is a little bit of a "cheat" as we would have to pass in the "Context" or equivalent to "Read" to provide it access to the underlying file system. The Context argument could presumably be supplied automatically as part of the syntactic sugar provided by the "shell" if desired.

Map/Reduce in ParaSail; Parameterized operations

The Map/Reduce paradigm popularized by Google has a long history. In APL, there is a reduction operator "/", which can be combined with an operator like "+" to reduce a vector to a scalar, by summing its individual members. That is "+/ V" adds up the elements of V producing a scalar sum. To include a map operation, you could simply insert the name of the scalar->scalar function of interest in the middle, and you get the map-reduce functionality. For example, "+/ V*2" would produce the sum of squares of the vector V ("*" is exponentiation in APL, "x" is used for multiplication).

In Google's variant of Map/Reduce, the input is a vector of key/value pairs, and the map operation takes one key/value pair and produces as output a list of key/value pairs. The reduce operation takes all values produced by any map invocation with the same key and combines them to produce a single value, or optionally a list of values, to be associated with this (output) key.

A simple, parallel version of Map/Reduce can be implemented relatively straightforwardly in ParaSail, as a single function, parameterized by the input and output types of the "Map" function:

// ParaSail Function to perform Map-Reduce operation.

function Map_Reduce
  (function Map(Input is Any<>) -> (Output is Any<>);
   function Reduce(Left, Right : Output) -> Output;
   Inputs : Vector<Input>)  {Length(Inputs) > 0} -> Output is
       // Handle singleton directly, recurse for longer inputs
       if Length(Inputs) == 1 then
         return Map(Inputs[1]);
       else
         // Split and recurse
         const Half_Length := Length(Inputs)/2;
         return Reduce
           (Map_Reduce(Map, Reduce, Inputs[1..Half_Length]),
             Map_Reduce(Map, Reduce, 
        Inputs[Half_Length <.. Length(Inputs)]));
       end if;
end function Map_Reduce;

procedure Test() is  // Test Map_Reduce function -- compute sum of squares
    Print_Int(Map_Reduce
      (Map => lambda(X : Integer) -> Integer is (X**2),
       Reduce => "+",
       Inputs => [1, 2, 3, 4, 5, 6]));
end procedure Test;

In ParaSail, the parameters in any call can be evaluated concurrently, so the two operands in the call on Reduce, which are recursive calls on Map_Reduce, will become separate pico-threads, allowing the Map_Reduce to be executed using a binary tree of pico-threads, providing significant potential for parallelism.

A couple of things to notice about the ParaSail implementation.  One key feature is that one parameter of an operation may provide type parameters for a later parameter.  In this case, the Map parameter has two type parameters, indicated by the use of the "type_name is interface_name<>" notation.  This says that the type (which must be an instance of module that implements interface_name) of the corresponding parameter of the actual Map function is henceforth available as type_name for use in later parameters and within the body of the operation.  It would be possible to make these instead be type parameters of an enclosing module, but it is more natural (and in some cases more powerful) to have the type parameters determined by the actual operation provided.  C++ provides a similar capability with template functions, where there is no need to explicitly specify the function template arguments, since the compiler can generally deduce the types from the call on the function, but the type parameters are not generally available outside the template function itself.  In ParaSail, the actual operation passed in for a parameter like Map can determine types that are to be used for later parameters (such as Reduce and Inputs) to the module or operation of which they are a parameter.

A second feature to notice is the use of an anonymous lambda construct in the call on Map_Reduce within the Test procedure, which allows a relatively simple operation (such as squaring) to be created at the point of call.  It would also be possible to declare a function named, for example, Square,  immediately before the call and pass that.  Note also that we can pass an operator such as "+" as the actual operation for the formal Reduce parameter.