THIS IS AN OUTDATED TOY VERSION OF REGLOCK !!!!!

Our latest work integrates our type system to Cyclone language

1  Introduction

This manual is meant to provide an informal introduction to Reglock.
Obviously, Reglock is a work in progress and we expect to make substantial changes to the design and implementation. Your feedback (and patience) is greatly appreciated.

2  Installation

2.1  Compilation

This section describes the compilation steps required to build reglock.

Prerequisites

This a list of software packages that must be installed on your system before compiling and installing Reglock.

• OCaml language.
• Make

Download reglock

Secure SVN access to lazy.softlab.ntua.gr is required to complete this step.

 svn co  svn+ssh://svn.softlab.ntua.gr/var/lib/svnrepos/svn-pl/internal/
    reglock/branches/mlock_impl

Change directory

Assuming that $REGLOCK_ROOT is the root path where mlock_impl is located then

 cd $RECLOCK_ROOT/mlock_impl/src

Compile Reglock

Make program is required in order to complete this step.

make

Run examples (Optional)

A new executable file named "f" should appear in $REGLOCK_ROOT/mlock_impl/src

./f ../tests/testtype.x

or you could run test cases that should fail :

./f ../tests/testtype_fail.x

3  Compiler

3.1  Options

This section describes the Reglock compiler options.Make sure you have completed Section 2 before proceeding.

Compiler options

[pgerakios@localhost src]$ ./f --help

Parsing args ...
 -I Append a directory to the search path
 -s Specify compilation stage: 0 = Parse , 1 = Binding , 
            2 = Type-checking , 3 = Interpret
 -v Specify verbosity level: 0 = None , 1 = Some ,
        2 = More , 3 = Lots
 -help  Display this list of options
 --help  Display this list of options 

Compilation stage

Reglock is a front-end compiler and interpreter. This option allows to skip some compilation steps. Option s (for stage) can take the following values

• 0 : Only parsing is performed.
• 1 : Only parsing and binding analysis is performed.
• 2: Only parsing,binding and type-checking is performed.
• 3: All four stages are performed: parsing,binding,type-checking and interpretation are performed.

Example: If you don’t want to enter the type-checking and interpretation stage you can specify the "-s 1" option.

[pgerakios@localhost src]$ ./f   -s 1 ../tests/testtype.5
Parsing args ...
Parsing file ../tests/testtype.5 [OK]
Binding ...  [OK]
Compilation successful.

Verbosity level

The compiler may become quite verbose mainly at the type-checking stage. The default value is "0" and the maximum value is "3".

• 0 : Output error messages only
• 1 : Reserved for future use
• 2 : For each function display the (1) function body (2) Ascripted type (3) "Inferred" type and the corresponding input output effects
• 3 : Same as 2 but display for each expression the full typing derivation.

Example:

[pgerakios@localhost src]$ ./f  -s 2 -v 2 ../tests/testtype.5

Parsing args ...
Parsing file ../tests/testtype.5 [OK]
Binding ... [OK]
Type-checking ...

Checking --> printInt  =  \ x. () as {} int -> unit {}
Ascripted type:  {} int -> unit {}

Checking --> printRgn  =  \ 'r. \ x. () as {} rgn('r) -> unit {}
Ascripted type:  Forall 'r. {} rgn('r) -> unit {}

Checking --> printIntRef  =  \ 'r. \ x. () as {} ref(int,'r) -> unit {}
Ascripted type:  Forall 'r. {} ref(int,'r) -> unit {}

Checking --> main  =  \ 'H. \ hrgn. newrgn 'r,x @ hrgn in ((thread1 ['r]) x $);rcapdec hrgn as {('H,1,bot,)} rgn('H) -> unit {('H,0,bot,)}
Ascripted type:  Forall 'H. {('H,1,bot,)} rgn('H) -> unit {('H,0,bot,)}

Checking --> thread1  =  \ 'r. \ x. rcapdec x as {('r,1,bot,)} rgn('r) -> unit {('r,0,bot,)}
Ascripted type:  Forall 'r. {('r,1,bot,)} rgn('r) -> unit {('r,0,bot,)}  [OK]

Interpretation

Once the type-checking stage has completed successfully the interpreter takes action: The interpreter is by default on verbose mode 3 so you should expect lots of output. The intepreter basically picks a thread of execution, evaluates (single-step semantics) the thread’s expression and prints out the following:

• The state of global/max handles (tid = thread id , rid = region id, lid = lock id) and a snaphot of the region hierarchy after evaluating one of the threads.

  Example:

   
  ----------------------------------
  Last tid=2 Last rid = 1 Last lid = 6 Heap :
  (R0,1,-1,0)= {}||{(R1,1,0,2)= {L6 |-> null,L5 |-> (10,loc2),
  L4 |-> null,L3 |-> (10,loc2),L2 |-> (7,loc1),
  L1 |-> (5,null)}||{}} 
  

  A region header is denoted as (Rx,n₁,n₂,n₃) where x is the region id, n₁ is the region reference count , n₂ is the lock count for this region and n₃ is the thread owner id (it may be ignored when n₂  =  0. Region contents are displayed and within curly brackets which are delimited by two consequtive vertical bars. A region consists of a private heap (the first set of curly brackets in the example above), which is a list of locations (Lx, where x  ∈  1...n) mapped to program values. The remaining contents denote subregions which have the same recursive structure.

• The interpreter picks randomly a thread to execute.

  Example:

  Scheduling thread 1.
  

  Note that 1 is not the thread id but the first thread in the scheduler’s list.

• The intepreter then prints debugging messages such as

  Example:

  @@@@@@@@ Cann't free rgn0 (thread 0)
  

  This message implies that thread id 0 is about to deallocate region 0 (main region) but it has detected that other threads own this/child regions so it busy-waits until it is possible to deallocate region 0.

• I/O side-effects are printed if an I/O operation is invoked (e.g printInt )

  Sideffects:
  Thread[2] ==> 5
  

• A list of threads and their corresponding expressions is then printed

  Thread id = 0
  rcapdec rgn0
  
  
  Thread id = 2
  rcapdec (rgn1,(10,loc2)).1 
  

• Finally at the end of the interpretation loop an I/O strings produced during program execution is displayed in a total order.

  Program I/O:
  
  Thread[1] ==> 10
  Thread[1] ==> 7
  Thread[1] ==> 5
  Thread[2] ==> 10
  Thread[2] ==> 7
  Thread[2] ==> 5 
  

3.2  Syntax

 toplevel :
    EOF
  | def ID = TopFunc ; toplevel
  | def TVarList = TopType ; toplevel
 
 TVarList:
     'ID 
  |  'ID , TVarList

 TopType:
    Type
  | \ ( TVarList ).Type

 TopFunc:
   \ ID . Term as Type
  | \ TVarList . TopFunc

 Capability: 
    bar(n)
  | *
  | bot
  | n

     
Effect:
      ( 'ID , Capability , Capability , TVarList )
    | ( 'ID , Capability , Capability  )
    | ( TVarList )
    
EffectList:
 | Effect EffectList

TypeDef:
 |  LBRACKET TVarList RBRACKET 
 
AtomicType:
     int
   | ()
   | rgn ( 'ID ) 
   | ref ( Type , 'ID ) 
   | ref ( Type , 'NULL ) 
   | { EffectList } Type -> Type {  EffectList }
   | \ 'ID . Type
   | exists 'ID ( 'ID , TVarList )  . Type
   | 'ID TypeDef

TypeX:
    AtomicType
  | AtomicType * TypeX 
  | ( TypeX )

 Type:
   TypeX

 Term:
    AppTerm 
  | !Term 
  | -Term 
  | not Term 
  | if Term then Term else Term 
  | while Term do Term
  | open Term 'ID , ID in Term
  | pack 'ID, Term as Type 
  | new Term @ Term
  | newrgn 'ID,ID @ Term in Term
  | rcapi Term
  | rcapd Term
  | lcapi Term
  | lcapd Term
  | let ID = Term in Term
  | Term binop Term 

Scope:
  | $

Assign:
  | COLON := Term

AppTerm :
    PathTerm Assign
  | AppTerm PathTerm  Scope
  | AppTerm [ 'ID  ]

PathTerm:
   PathTerm.n
  | AtomicTerm

TermSeq : 
    Term
  | Term , TermSeq
  | Term ; TermSeq

ParenSeq:
  | TermSeq

AtomicTerm:
    ( ParenSeq )
  | ID
  | n
  | null
 
 

4  FAQ

Question

why are parentheses necessary around ’r below?

 def 'List = \ ('r). ref (int * 'List ['r], 'r); 
 

Answer: We only allow top-level region polymorphism in user-defined types. Therefore, when there exist several region names (a list of names) then the parenthesis aid in delimiting those regions. Consider a List whose nodes are allocated at different regions:

        def 'List = \ ('r1,'r2). ref (int * 'List ['r2], 'r1);
 

Index

This document was translated from L^AT_EX by H^EV^EA.