Section J.1) Control flow in -core

In this section we will discuss:
  • return from within claims
  • break, etc. from within claims

return from within claims

The -core language discussed so far does not take control flow into account for the embedded C code. This requires the programmer to refrain from return/breaking from within claims. E.g.,

....
// A variable r protected by R
#>
int r = 0;
<#

Func int f(int k) {
  claim R {
    #>
    if (r>10) 
       return r;
    else {
       r = r + 1; 
       return r;
    }
    r = r + 1; // intentionally some dead code here
    <#
  }
}
....

This code would exit the function Func f without releasing the claimed resource. (This clearly breaks the functionality of the system.)

Using the vanilla -core language we (as a programmer) would have to re-write the code into something like:
....
// A variable r protected by R
#>
int r = 0;
<#

Func int f(int k) {
  #> int local_r; <#
  claim R {
    #>
    if (r>10) 
       local_r = r;
    else {
       r = r + 1;
       local_r = r; 
    }
    //  r = r + 1; manually removing the dead code !
    <#
  }
  return local_r;
  ....
}
....

Since we cannot return within the claim, and we cannot access r outside the claim, we are forced to infer a local copy (local_r). The returning semantics of C has to be fully understood, and we have to take that into account and manually disable/remove the dead code. (This is just a trivial case, in practise it may require quite some attention of the programmer.)

This is kind of manual code transformations required when dealing with critical sections, is by no means unique to -core, (whenever critical sections are used, you are not allowed to exit within a critical section without ensuring that locks are released, moreover, access to protected resources (like the variable r) should never be made outside the critical section.

However, in the following we show an extension to -core solving this problem in an elegant manner.
....
// A variable r protected by R
#>
int r = 0;
<#

Func int f(int k) {
  claim R {
    #>
    if (r>10) 
       #> claim_return <#r#>;
    else {
       r = r + 1; 
      #> claim_return <#r#>;
    }
    r = r + 1; // intentionally some dead code here
    <#
  }
  ....
}
....

Notice:
  1. 1) we do not explicitly define a local copy for the return value
  2. 2) the C semantics are preserved, we do not need to restructure the program, else then use the new construct claim_return

In order to achieve this, we need the -core compiler to:
  1. 1) infer a return variable "return_val" of the correct return type in (this case int)
  2. 2) for each claim_return
    • keep track of the (nested) claims
    • assign the return variable
    • release the claims (unlock the corresponding locks in LIFO order)
    • perform a C return of "return_val"

Further details on the code generation: In C return can occurs as a single statement in a conditional (if) statement. The generated code will be a sequence of C statements, hence requires a { ... } context.

Other design choices:
  • If claim_return occurs outside a claim, we have the choice to either report this as an error, warning or simply replace it by a "native" C return (for the implementation I opted for the last case).
  • One could also consider the syntax (we could reuse the C return keyword, but I chose to give it a new name to indicate the difference...)
  • One could also consider to "float" the locking mechanism to the -core programmer, allowing the explicit locking/unlocking of resources. I believe this is would be a really bad thing for several reasons.
    1. Easy to forget some lock when programming, revising code.
    2. Easy to miss the LIFO order (nesting) of resources. Then correct nesting is an outset for the programming model and the underlying schedulers / run-time systems.
    3. It would add to the complexity of the programming in -core. We like to keep the model simple.

break, etc. from within claims

In C, you may voluntarily exit from within a loop or switch construct using the break statement. In -core you may embed claims within both loops and switches (in fact -core and C statements may be arbitrarily mixed/interleaved).

Following the reasoning above (the return discussion), we now see that also break might (if not used carefully) lead to incorrect -core programs. In the following we introduce a "partial" solution.

// FuncCore1.core
// Per Lindgren (C) 2014
//
// Showcasing 
//  claim_return (safe return form within claims)
//  claim_break, claim_continue, claim_goto
Func int f(int k) {
  #> int i = 0; <#
  claim R {
    #> if (k == 0) <#
      claim_return #>-1<#;
    #> while (i < 10) { <#
      claim Q {
        #> i = i + 1; <#
        #> if (k == 1) <#
          claim_return #>0<#; // return 0
        #> if (k == 2) <#
          claim_break;        // return 1
        #> if (k == 3) <#
          claim_continue;     // return 10
        #> if (k == 4) <#     
          claim_goto 2 label; // return 1  
      }
      #> printf("i = %d, ", i); <# // run if k == 5
    #> } <#
  }
  #>label:<#
  claim_return #>i<#;
}

Reset {
  #> 
  for (int x = 0; x < 3; x++) {
    printf("iteration x %d\n", x); // (in)sanity check...
    
    for (int k = 0; k < 6; k++) {  // check the different cases
      int i = <# sync f(k); #>;
      printf("\nf(%d) = %d\n", k, i );
    }
  }
  <#
}


In order to achieve this, we need the -core compiler to:
  • for each claim_break claim_continue, claim_goto
    • keep track of the (nested) claims
    • release the topmost X claim(s) (unlock the corresponding lock(s) in LIFO order)
    • perform the C break/continue/goto

Why only a partial solution? Recall, the -core compiler is in general not parsing/understanding the embedded C code. Hence there is no way for -core to know, the number of claims (nesting depth) that should be released on each break.

A reasonable trade-off is to require some collaboration by the programmer in this case. We introduce claim_break/continue/goto X, where X is the (optional) nesting depth. E.g., claim_break 2, would release two nested claims, while claim_break by default release just the last (innermost) one. (Recall, the nested/LIFO behaviour of claims in RTFM).

Word from the author:

As already discussed, we only scratch the surface of flow control in -core. Often this is fine, but as soon as claims are to exited from within the critical section, we need to take special considerations, unless we will leave a claim unreleased. To this end we have the option either to require the programmer to structure code in such a way this never happens, or provide the necessary means to safely handle the problem.

We do not intend to make -core fully understand the control flow of C (to that and a complete C front-end would be required for the parsing). Instead we tackle the problem where they occur (we support returns and breaks, continues and gotos).

Whereas -core is C-complete, it implies that any source program and/or library can be made to work with and under -core, but it requires that if you use it inside -core construct (such as claims) that you follow the RTFM execution semantics. The addition of claim_return, claim_break etc. facilities this process, while less restructuring of the original C code is required, but still you as a programmer has the responsibility of the correctness for all embedded (or linked) C code.

The story is different when going into the -cOOre language. Here the compiler can gain the full understanding and knowledge of the control flow, and hence generate code that is ensured to follow the RTFM semantics.

In that light, -core is seen just as an intermediate representation. However, w.r.t. usability, the ability to embed C code is still there (as bindings to -cOOre objects). To this end I found it worthwhile to invest in facilitating the migration.

/Per Lindgren, founder of RTFM, October 8th 2014


Last edited Oct 9, 2014 at 3:26 PM by RTFMPerLindgren, version 3