Keiko Nakata

Andrei Sabelfeld

Securing Class Initialization

Keywords:

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Language-based concepts and techniques are becoming increasingly popular in the context of security [Koz99,SMH00,WAF00,SM03,Ler03,MSL + 08,Cro09,Fac09] because they provide an appropriate level of abstraction for specifying and enforcing application and language-sensitive security policies. Popular examples include Java stack inspection [START_REF] Wallach | The security architecture formerly known as stack inspection: A security mechanism for language-based systems[END_REF], which enforces a stack-based access-control discipline, and Java bytecode verification [START_REF] Leroy | Java bytecode verification: algorithms and formalizations[END_REF], which traverses bytecode and verifies its type safety, as well as web language-based mechanisms such as Caja [MSL + 08], ADsafe [START_REF] Crockford | Making javascript safe for advertising[END_REF], and FBJS [START_REF]Facebook[END_REF], which use program transformation and language subsets in order to enforce sandboxing and separation properties.

Language-based information-flow security [START_REF] Sabelfeld | Language-based information-flow security[END_REF] is concerned with specifying and enforcing security policies for information flow via language constructs. There has been much recent progress on understanding information flow in languages of increasing complexity [START_REF] Sabelfeld | Language-based information-flow security[END_REF], and, consequently, information-flow security tools for languages such as Java, ML, and Ada have emerged [MZZ + 10, [START_REF] Simonet | The Flow Caml system. Software release[END_REF][START_REF]Praxis High Integrity Systems. Sparkada examinar. Software release[END_REF]. In particular, information flow in object-oriented languages has been an area of intensive development [Mye99,BS99,BCG + 02,ABF03,BFLM05,BN05,ABB06,Nau06,BRN06,HS09]. However, it is surprising that the impact of class initialization, being an important aspect of object-oriented programs, has received scarce attention in the context of security. In a language like Java, class initialization is lazy: classes are loaded as they are first used. This introduces challenges for information-flow tracking, in particular when class initialization may trigger initialization of other classes, which, for example, may include superclasses. Additional complexity is introduced by exceptions raised during initialization. Exceptions may be exploited to leak secret information.

Because of its power, Java's class loading mechanism [START_REF] Liang | Dynamics class loading in the Java virtual machine[END_REF] is a target for our model. A class is loaded, linked and initialized lazily on demand when the class is actively used for the first time [START_REF] Lindholm | The Java TM Virtual Machine Specification[END_REF] 3 . Moreover the programmer may define applicationspecific loading policies. Class loading constitutes one of the most compelling features of the Java platform.

This paper turns the spotlight on security implications of class initialization (and loading and liking, which are prerequisites for initialization). We discuss the subtleties of information propagation when classes are initialized. The key issue is that class initialization may perform side effects (such as opening a file or updating the memory). The side effects may be exploited by the attacker who may deduce from these side effects which classes have been (not) initialized, which is sometimes sufficient to learn secret information.

We propose a formalization that illustrates how to track information flow in presence of class initialization by a type-and-effect system for a simple language. By ensuring that classes may not be initialized inside conditionals and loops that branch on secret data, the type-and-effect system guarantees security in a form of noninterference [START_REF] Goguen | Security policies and security models[END_REF]. We show how to extend the formalization to a language with exception handling. The only approach we are aware of that actually considers class initialization in the context of information-flow security is Jif [Mye99,MZZ + 10]. However, Jif's restrictions on code initialization are rather severe: this code is restricted to simple constant manipulation that may not raise any exceptions. Our treatment of class initialization is more liberal than Jif's and yet we demonstrate that it is secure. We argue that this liberty is sometimes desired in scenarios such as server-side code.

Background

This section presents informal considerations that lead up to a formalization in the following sections. For illustration purposes, we use a simple subset of Java with classes that contain static fields. We assume variables and class fields are partitioned into high (secret) and low (public). We assume that l and h are typical low and high variables, respectively. The security goal is to prevent programs from leaking initial values of secret data into final values of public data. The context corresponds to a body of a conditional or loop. We say that the context is high if the guard depends on a secret (i.e., contains a secret variable or field) and low otherwise.

Consider the following two class definitions for class names C and D with low fields g and f , respectively:

class C { g = 1 } class D { f = 1/C.g }
Certainly the above definitions may be considered secure since no high data is involved. However, an attempt to instantiate an object of D may lead to an information leak:

P 0 : C.g := 0; if h = 0 then new D else skip
Indeed, the above program results in an error only when the high variable h initially contains 0, in which case the class D is initialized. Note that in the terminology we have introduced, the initialization occurs in high context. The attacker learns about the secret value of h by observing the termination behavior.

It is illustrative to compare the above program that leaks through termination behavior with the following one that does not:

P 1 : new D; C.g := 0; if h = 0 then new D else skip
In this latter program, D is initialized before the assignment. More importantly, D has been initialized before it is used in high context: the second use does not incur any initialization activities.

In Java, when initialization of a class has completed abnormally by throwing some exception, the class is marked as erroneous. Initialization of a class in an erroneous state is not possible [LY99, Ch. 2]4 . This makes initialization failure persistent in the sense that when initialization of a class failed on it first (active) use, then it will fail on the second use irrespective of the state in which the second initialization is attempted5 . Catching initialization errors introduces a delicate scenario of information leaks. For instance, consider the following program: The above program successfully terminates irrespective of the initial value at h, and the final value at l indicates whether h was 0 or not.

P 2 : C.g := 0; if h = 0 then (
Security might be compromised within correct, i.e., error-free, programs. Moreover class hierarchy also may impact on the security: before a class is initialized, its superclasses are initialized. For instance, consider class definitions below, involving only low fields.

class

C 0 { g = 1 } class D 0 { f = C 0 .g++ } class D 1 extends D 0 {}
The next program leaks the initial value of h into the final value of C 0 .g.

P 4 : new C 0 ; if h = 0 then new D 1 else skip
Combining the two previous programs yields a scenario, where class hierarchy and persistence of initialization failure cooperate to leak information:

class C 0 { g = 1 } class D 0 { f = 1/C 0 .g } class D 1 extends D 0 {} P 5 : C 0 .g := 0; if h = 0 then (try new D 1 catch skip) else skip; C 0 .g := 1; try new D 0 ; l := 1 catch l := 0
Again the resulting program always terminates normally and reflects secret input values in the public results. The bottom line is that class initialization may perform side effects, causing information to leak. One rather conservative approach to securing class initialization is to eliminate any possibilities of side effects during initialization and disallow errors due to initialization to be caught, an approach taken in Jif [Mye99,MZZ + 10]. This approach rules out, among other, read and write access to instance as well as static fields, method calls and object creation during initialization. For example, a static field of a reference type may only be initialized to null, which would exclude some standard Java APIs [Sun], such as (java.lang.)Boolean and String, etc. Indeed Jif restricts (class) field initializers to simple constant manipulation that may not raise any exceptions. While it is rarely good practice to catch initialization errors within ordinary methods, such as methods in libraries, there are several scenarios where it is good practice to catch them, such as in server applications to avoid crashing the entire system due to third party applications or to log messages. For instance, Fortress, the primary product from the Excalibur software project [Exc], catches LinkageError and rethrows an object of a subclass of Exception, which may in turn be caught and logged.

This paper goes ahead to propose and formalize a different approach: we restrict class initialization in high contexts but allows side effects during initialization. Section 4 develops a type-and-effect system for a simple language, defined in Section 3. The typeand-effect system ensures a class has been initialized before it is used in high contexts and, as we show, guarantees information-flow security. Moreover, Section 5 shows how to scale our approach, when initialization errors are permitted to be caught. Section 6 discusses related work, and Section 7 concludes.

We define the language for our formal study by the following syntax: A state (or store), ranged over by σ, maps variables to integers and class names to abstract class objects. An abstract class object, or simply class object, denotes the loaded status of a class name C in a state σ: C is uninitialized in σ when σ(C) = •; initialization is in progress or has been successfully completed when σ(C) = {f 0 = n 0 , . . . , f k = n k }, where f i 's are the fields of the class C; C has failed to initialize when σ(C) = •. We write uninitialized (σ) to denote the set of uninitialized classes in σ, i.e., {C | σ(C) = •}, initialized (σ) the set of classes of which initialization is in progress or has been completed in The small-step operational semantics for the statements is given in Fig. 2. The onestep reduction relation σ, s → σ , s states that in the state σ the statement s one-step reduces to s with the next state being σ . The relation σ, s → σ , • states that the statement s in the state σ signals an error in the state σ . We write σ, s ↓ σ , stating that s in the initial state σ successfully terminates in the final state σ . Or, σ, s ↓ σ if σ, s → * σ , skip , where → * denotes the reflexive and transitive closure of →. Finally Fig. 3 defines the class initializer. If initialization of the class has been initiated and has not failed, i.e., σ(C) = {f 0 = n 0 , . . . , f n = n k }, then the initializer immediately returns. This covers both the cases that initialization is in progress and that initialization has been successfully completed. If initialization has previously failed, therefore the class object is in erroneous state, i.e., σ(C) = •, then initialization is not possible. Otherwise, the initialization is initiated: the fields are first set to default values, namely 0, then updated according to their initializing expressions. The initialization may fail, in which case the class object is marked erroneous.

σ, i.e., {C | σ(C) = {f 1 = n 1 , . . . , f k = n k } for some f 1 , . . . , f k , n 1 , . . . , n k ,
(σ, n) ↓ (σ, n) (σ, x) ↓ (σ, σ(x)) (σ, e0) ↓ (σ , n0) (σ , e1) ↓ (σ , n1) n0 op n1 = n (σ, e0 op e1) ↓ (σ , n) (σ, e0) ↑ σ (σ, e0 op e1) ↑ σ (σ, e0) ↓ (σ , n0) (σ , e1) ↑ σ (σ, e0 op e1) ↑ σ (σ, e0) ↓ (σ , n0) (σ , e1) ↓ (σ , n1) n0 op n1 = • (σ, e0 op e1) ↑ σ ρ(σ, C) ↓ σ (σ, C.f ) ↓ (σ , σ (C.f )) ρ(σ, C) ↑ σ (σ, C.f ) ↑ σ

Specifying and Enforcing Security

We now introduce a security condition for our language and then develop a security type system for statically guaranteeing this condition.

Security condition

As before, we assume a simple security lattice [START_REF] Denning | A lattice model of secure information flow[END_REF] consisting of only two levels low (public) and high (secret), with low high. Metavariables and pc range over security levels. Then a security environment Γ is a finite mapping from variables and pairs (C, f ) of a class name and a field name of the class to their security levels. We extend Γ to expressions by assuming an expression is mapped to the least upper bound of the security levels that occur in it. Again, for the sake of notational simplicity, we assume a fixed security environment Γ in what follows.

(σ, e) ↓ (σ , n) σ, x := e → σ [x → n], skip (σ, e) ↓ (σ , n) ρ(σ , C) ↓ σ σ, C.f := e → σ [C.f → n], skip (σ, e) ↑ σ σ, C.f := e → σ , • (σ, e) ↓ (σ , n) ρ(σ , C) ↑ σ σ, C.f := e → σ , • σ, skip; s → σ, s σ, s0 → σ , s 0 σ, s0; s1 → σ , s 0 ; s1 σ, s0 → σ , • σ, s0; s1 → σ , • (σ, e) ↓ (σ , n) n = 0 σ, if e then st else s f → σ , st (σ, e) ↓ (σ , 0) σ, if e then st else s f → σ , s f (σ, e) ↓ (σ , n) n = 0
σ, while e do st → σ , st; while e do st (σ, e) ↓ (σ , 0) σ, while e do st → σ , skip for any x such that Γ (x) = low , σ(x) = σ (x); uninitialized (σ) = uninitialized (σ ), initialized (σ) = initialized (σ ), and also failed (σ) = failed (σ ); for any C and f such that

(σ, e) ↑ σ σ, Q[e] → σ , • where Q ::= x := [] | if [] then st else s f | while [] do st
σ(C) = {f0 = n0, . . . , f k = n k } ρ(σ, C) ↓ σ σ(C) = • ρ(C, σ) ↑ σ σ(C) = • CT (C) = class C {f0 = e0, . . . , f k = e k } σ[C → {f0 = 0, . . . , f k = 0}], C.f0 := e0; . . . ; C.f k := e k ↓ σ ρ(σ, C) ↓ σ σ(C) = • CT (C) = class C {f0 = e0, . . . , f k = e k } σ[C → {f0 = 0, . . . , f k = 0}], C.f0 := e0; . . . ; C.f k := e k ↑ σ ρ(C, σ) ↑ σ [C → •]
Γ (C, f ) = low and C is in initialized (σ), σ(C.f ) = σ (C.f ).
We adopt a commonly-used baseline policy of termination-insensitive noninterference [VSI96,SM03,PS03]. Intuitively, a program satisfies noninterference if for any two initial memories that agree on public data, whenever the program runs that start in these memories terminate, then these runs result in the memories that also agree on public data. This policy is an appropriate fit for batchjob programs, where leaks due to (non)termination are ignored because they may leak at most one bit per execution [START_REF] Askarov | Termination-insensitive noninterference leaks more than just a bit[END_REF].

Definition 1. A statement s satisfies termination-insensitive noninterference if, for any low-equivalent states σ 0 and σ 1 , σ 0 , s ↓ σ 0 and σ 1 , s ↓ σ 1 imply σ 0 = low σ 1 .

Type system

Class initialization potentially performs low side effects. Therefore, we are going to prohibit class initialization in high contexts. Our type system essentially performs a must-analysis: a class must have been initialized before it is used in high contexts.

Fig. 4 presents typing rules for expressions. The judgment pc e : δ → δ states that the expression e is typable at the security level pc with the effect type δ → δ . The pretype δ and the posttype δ , respectively, represent the classes that must have been initialized before and after the expression is evaluated. Effectively pc e : δ → δ is read that the class names that occur in e must be in δ when pc is high, and δ is the union of the class names that occur in e and δ. The type system may be made more permissive by computing, for each class C, the set of the classes that are necessarily initialized during the initialization of C.

Fig. 5 presents typing rules for statements. The judgment pc s : δ → δ is read similarly to that for expressions. For example, the rule for assignment prevents explicit flows (such as l := h), implicit flows [DD77] via control structure (as in if h = 0 then l := 0 else l := 1) in a standard fashion [DD77,VSI96,SM03]. In addition, the effect type information is propagated from the expression to command level, and class initialization in high contexts is ruled out. For the posttype of if-statement, we take the intersection of the posttypes of the branches, collecting classes that must have been initialized irrespective of which branch is taken. Similarly, the posttype of whilestatement only includes classes initialized by evaluating the boolean guard, since the loop-body might not be executed at all.

To state soundness with respect to the security condition, we must ensure that the type environment Γ is consistent with the class table CT . The existence of a well-formed environment ensures typability of the class table.

pc n : δ → δ pc x : δ → δ pc e0 : δ → δ0 pc e1 : δ → δ1 pc e0 op e1 : δ → δ0 ∪ δ1 low C.f : δ → δ ∪ {C} C ∈ δ high C.f : δ → δ
The type system is sound with respect to termination-insensitive noninterference:

Lemma 1. Suppose Γ is well-formed with respect to CT . If pc s : δ → δ and σ 0 = low σ 1 and δ ⊂ initialized (σ 0 ) ∪ failed (σ 0 ) and σ 0 , s ↓ σ 0 and σ 1 , s ↓ σ 1 , then δ ⊆ initialized (σ 0 ) ∪ failed (σ 0 ) and σ 0 = low σ 1 .

Corollary 1. If pc s : ∅ → δ then s satisfies noninterference. This section extends our system with an exception handling mechanism. The Java virtual machine throws an object that is an instance of a subclass of LinkageError when a loading, linkage, preparation, verification or initialization error occurs [START_REF] Gosling | The Java TM Language Specification[END_REF]Ch. 11]. LinkageError is a subclass of Error, rather than Exception. Error is designed in principle to indicate serious problems, and ordinary applications, such as library programs, are not expected to catch Error . However, as we argued in Section 2, there are several scenarios where catching Error is desirable such as in server applications to avoid crashing the entire system or to log messages. Therefore, we are motivated to develop a security type system which allows errors due to class initialization to be caught, while rejecting attacks that leak information through exception handling.

Operational semantics

We extend the syntax of the statements with try s 0 catch s 1 , whose operational semantics is given in Fig. 6.

Type system

Fig. 7 and Fig. 8 give typing rules for expressions and statements, respectively. We extend the type environment Γ to map class names to the security levels of the exceptions that may be raised during initialization. We have to adjust the definition of well-formed type environments: Definition 3. A type environment Γ is well-formed with respect to a class table CT if, for any class name C and a field name f of C such that CT (C) = class C {. . . , f = e, . . .}, we have

-Γ (e) Γ (C, f ); -if low e : δ → δ :: then Γ (C).
We note that initialization failure of a class having high fields may be low and a class having only low fields may be high, as the following example illustrates:

class C 0 { g = 4, f = 1 op 0 } class C 1 { g = 1 op 0, f = 1 } class C 2 { f = C 1 .f } A type environment Γ such that Γ (C 0 ) = Γ (C 0 , f ) = Γ (C 1 , f ) = Γ (C 2 , f ) = low and Γ (C 1 ) = Γ (C 2 ) = Γ (C 0 , g) = Γ (C 1 , g) = high
is well-formed with respect to the class table corresponding to the above class definitions.

Having noticed the above subtlety, the typing rules in Fig. 7 and Fig. 8 are straightforward adaptation from type systems that track information flow in the presence of exceptions (e.g., [Mye99,PS03,HS06,AS09]). The new form of judgment pc e : δ → δ :: for expressions (resp. pc s : δ → δ :: for statements) indicates the level of an exception that the expression e (resp. the statement s) may throw in the context pc.

For expression typing, pc e : δ → δ :: low is derivable if either e does not throw an exception, or else pc is low and for any class C that occurs in e, Γ (C) = low and, for any subexpression e of e that is an operand of op, Γ (e ) = low . Suppose Γ (x) = high, for instance, then high x : ∅ → ∅ :: low and low

x op n : ∅ → ∅ :: high are derived. Notice that the security level of x is propagated to the security level of an exception only if the value of x may affect whether or not an exception is thrown.

We look at the inference rules for typing of statements. Since skip does not throw an exception, its exception level is low. The exception level of an assignment x := e is that of the expression e at pc. For the exception level of an assignment to a field of a class, C.f := e at low program context, we take the upper bound of the exception level of e at low and Γ (C). More importantly, the exception level of C.f := e in high program context is necessarily high, even if e does not throw an exception. This is because initialization of C may be triggered and fail, if it has previously failed, as illustrated by the following program, where f is low and g is high.

class C { f = 1/0, g = 1 } try C.f := 1 catch skip; try (if h = 0 then C.g := 0 else skip) catch l := 1
The above program is insecure and indeed rejected by our type system.

For the sequence statement, we prohibit s 1 from performing side effects lower than the level of exceptions that s 0 may throw. Rules for if-and while-statements are similar. The exception levels of the boolean guards are propagated to branches. In try-statement, the catch clause must not perform side effects lower than the exception level of the try block. Note that the exception level of the whole statement is 1 , the exception level of the catch clause.

Proposition 1. If pc s : ∅ → δ :: then s satisfies noninterference.

We now come back to the examples in Section 2. Since none of the class definitions from Section 2 involves high fields, they are typable with respect to an obvious type environment Γ mapping all the classes and class-field pairs to low. We keep the convention that Γ (l) = low and Γ (h) = high. All the programs but P 1 are not typable. For P 1 , we have low P 1 : ∅ → {D} :: high. Note that the programs P 0 , P 1 and P 2 satisfy noninterference, but P 3 , P 4 and P 5 do not (assuming the operational semantics is appropriately extended to take class hierarchy into account.)

Related Work

A survey [START_REF] Sabelfeld | Language-based information-flow security[END_REF] on language-based information-flow security contains an overview of the area. Most related to ours is work on tracking information flow in object-oriented languages and on information-flow controls in the presence of exceptions.

Objects To the best of our knowledge, the only information-flow mechanism that addresses class initialization is the one implemented by Jif [Mye99,MZZ + 10], a compiler for Java extended with security types. As discussed earlier, Jif is rather conservative about class initialization code. This code is restricted to simple constant manipulation that may not raise any exceptions. As mentioned earlier, sometimes it is desirable to lift these restrictions.

Much other work has been done on information-flow security for object-oriented languages. Although none of the approaches directly addresses problems with class initialization, we nevertheless discuss some recent highlights.

Barthe and Serpette [BS99] present a type system for enforcing information-flow security in a simple object-oriented language based on the Abadi-Cardelli functional object calculi [START_REF] Abadi | A Theory of Objects[END_REF]. Bieber et al. [BCG + 02] apply model-checking for securing information flow in smartcard applets.

Avvenuti et al. [START_REF] Avvenuti | Java bytecode verification for secure information flow[END_REF] suggest an information-flow analysis in a language similar to Java bytecode. Bernardeschi et al. [START_REF] Bernardeschi | Checking secure information flow in java bytecode by code transformation and standard bytecode verification[END_REF] check information-flow security in Java bytecode by a combination of program transformation and bytecode verification. These two approaches assume fixed security levels for classes. This might not be a flexible choice since it forces all instances and attributes to conform to the class level. Another concern is the scalability of this choice in presence of inheritance.

Banerjee and Naumann [START_REF] Banerjee | Stack-based access control and secure information flow[END_REF] show how to guarantee noninterference by a typebased analysis for a Java-like imperative language with objects. Amtoft et al. [START_REF] Amtoft | A logic for information flow in objectoriented programs[END_REF] present a flow-sensitive logic for reasoning about information flow in the presence of pointers. Naumann [START_REF] Naumann | From coupling relations to mated invariants for checking information flow[END_REF] investigates invariant-based verification of informationflow properties in a language with heaps. Barthe and Rezk [START_REF] Barthe | Non-interference for a jvm-like language[END_REF] consider type-based enforcement of secure information flow in Java bytecode-like languages. Barthe et al. [START_REF] Barthe | Deriving an information flow checker and certifying compiler for java[END_REF] extend this work to derive an information-flow certifying compiler for a Java-like language.

Hammer and Snelting [HS09] develop a flow-sensitive, context-sensitive, and objectsensitive framework for controlling information flow by program dependence graphs. This approach takes advantage of similarities of information-flow and slicing analyses.

Exceptions As noted earlier, our treatment of exception handling draws on standard approaches from the literature (which we extend with the must-analysis). The intuition is if an occurrence of an exception in a statement may carry sensitive information, then there must be no publicly-observable side effects in either the code that handles the exception or in the code between the statement and the exception-handling block. Jif [Mye99,MZZ + 10] implements such a discipline. Based on a similar discipline, Pottier and Simonet [START_REF] Pottier | Information flow inference for ML[END_REF] propose a sound treatment of exceptions for ML.

Barthe and Rezk [START_REF] Barthe | Non-interference for a jvm-like language[END_REF] treat a single type of exceptions in a JVM-like language. Barthe et al. [START_REF] Barthe | A certified lightweight non-interference java bytecode verifier[END_REF] extend this approach to multiple types of catchable exceptions. Connecting this with security-type preserving compilation, Barthe et al. [START_REF] Barthe | Deriving an information flow checker and certifying compiler for java[END_REF] show how to securely compile a source language with a single type of catchable exceptions to the low-level language of Barthe and Rezk [START_REF] Barthe | Non-interference for a jvm-like language[END_REF].

Hedin and Sands [START_REF] Hedin | Noninterference in the presence of non-opaque pointers[END_REF] prove a noninterference property for a type system that tracks information flow via class-cast and null-pointer exceptions in a language with non-opaque pointers. Askarov and Sabelfeld [START_REF] Askarov | Catch me if you can: Permissive yet secure error handling[END_REF] show how to achieve permissive yet secure exception handling by providing the choice for each type of exception: either the traditional discipline discussed above or by consistently disallowing to catch exceptions. The actual choice for each kind of exception is given to the programmer.

Conclusion

Seeking to shed light on a largely unexplored area, we have presented considerations for and a formalization of secure class initialization. Our considerations highlight that class initialization poses challenges for security since controlling (the order of) side effects performed by class initialization is challenging. Hence, great care needs to be taken by information-flow enforcement mechanisms to guarantee security. One path, taken by Jif [Mye99,MZZ + 10], is to severely restrict class initialization code so that it may only manipulate constants in an exception-free manner. Arguing that it is sometimes too restrictive, we have explored another path: allow powerful initialization code, but disallow class initialization inside conditionals and loops that branch on secret data. This approach has the advantage that the side effects in class initialization do not have to be predicted since they may not carry sensitive information in the first place: the attacker may not deduce anything interesting from observing these side effects anyway.

Our formalization demonstrates the idea by a type-and-effect system for a simple language that enforces noninterference. To the best of our knowledge, it is the first formal approach to the problem of secure class initialization. (Soundness of Jif's class initialization is yet to be established.)

Future work includes an extension to handle class hierarchies. We believe our approach of ruling out class initialization in high contexts is sound in the presence of class hierarchies. To extend our technical results to class hierarchies, we only need to adjust the operational semantics so that when a class is initialized, all its (uninitialized) super classes are initialized. Based on the results of the paper, we are currently working on more sophisticated type systems that allow initialization of high classes in high contexts.

  Expressions e ::= n | x | e 0 op e 1 | C.f Statements s ::= skip | s 0 ; s 1 | x := e | C.f := e | if e then s t else s f | while e do s t Class definitions CL ::= class C {f 0 = e 0 , . . . , f k = e k } Metavariables x, n, C and f range over variables, integers, class names and field names, respectively. We assume given a binary partial operator op on integers, i.e., op may signal an error. We write n 0 op n 1 = • when op signals an error on operands n 0 and n 1 . A class definition class C {f 0 = e 0 , . . . , f k = e k } declares a class name C consisting of the (static) fields f i 's with e i 's being initializing expressions. Then a class

  and failed (σ) the set of classes that have failed to initialize, i.e., {C | σ(C) = •}. When the context ensures C is in initialized (σ), we may write σ(C.f ) to denote f -field of the class object for C in σ, i.e., σ(C.f ) = n where σ(C) = {. . . , f = n, . . .}, and σ[C.f → n] to denote the update of f -field of the class object for C in σ by n. Evaluation of expressions is given in Fig. 1. The relation (σ, e) ↓ (σ , n) states that the expression e in the state σ evaluates to the result n with the state being σ . The relation (σ, e) ↑ σ states that evaluating the expression e in the state σ fails in the state σ , signaling an error. The inference rules in Fig. 1 are straightforward except those for reading from a field of a class. Both read and write access to a field of a class C triggers initialization of C. Class initializer ρ(C, σ), to be defined below, initializes the class C in the state σ. If the initialization is in progress or has been successfully completed, written ρ(σ, C) ↓ σ , σ contains a class object for C and evaluation of C.f returns f -field of the class object. If the initialization fails, written ρ(σ, C) ↑ σ , so does the evaluation of C.f .

Fig. 1 .

 1 Fig. 1. Expression evaluation

Fig. 2 .

 2 Fig. 2. Operational semantics for statements

Fig. 3 .

 3 Fig. 3. Class initialization

Fig. 4 .

 4 Fig. 4. Typing of expressions

Fig. 5 .Fig. 6 . 1 Γ

 561 Fig. 5. Typing of statements

Fig. 8 .

 8 Fig. 8. Typing of statements for exception handling

  table CT is a (finite) mapping from class names to class definitions. A program is a pair (CT , s) of a class table and a statement. To lighten the notation, we assume a fixed class table CT hereafter.

The JVM specification permits the large flexibility as to the timing of loading and linking. But these activities must appear as if they happen on the class's (or interface's) first active use.

To be precise, the Class object representing the class is labeled as erroneous.

Initialization may recover for instance by resorting to garbage collection. But normally a class is eligible for unloading when the running application has no reference to the class.

Acknowledgments K. Nakata acknowledges the support of action IC0701 of COST, the Estonian Centre of Excellence in Computer Science, EXCS, financed mainly by ERDF, and the Estonian Science Foundation grant no. 6940. A. Sabelfeld is supported by the Swedish research agencies SSF and VR.


Jinhua Cui

Weiguo Wu
email: wgwu@xjtu.edu.cn

Shiqiang Nie

Jianhang Huang

Zhuang Hu

Nianjun Zou

Yinfeng Wang

Exploiting Cross-Layer Hotness Identification to Improve Flash Memory System Performance

Keywords: NAND flash memory, Endurance, Raw bit error rate, Threshold voltage, Cross-layer

Flash memory has been widely deployed in modern storage systems. However, the density improvement and technology scaling would decrease its endurance and I/O performance, which motivates the search to improve flash performance and reduce cell wearing. Wearing reduction can be achieved by lowering the threshold voltages, but at the cost of slower reads. In this paper, the access hotness characteristics are exploited for read performance and endurance improvement. First, with the understanding of the reliability characteristics of flash memory, the relationship among flash cell wearing, read latency and bit error rate is introduced. Then, based on the hotness information provided by buffer management, the threshold voltages of a cell for write-hot data are decreased for wearing reduction, while these for read-hot data are increased for read latency reduction. We demonstrate analytically through simulation that the proposed technique achieves significant endurance and read performance improvements without sacrificing the write throughput performance.

Introduction

In recent years, storage devices equipped with NAND flash memory have become widely used for a multitude of applications. Due to its high density, low power consumption, excellent IOPs performance, shock-resistance and noiselessness, NAND flash-based solid state drive (SSD) is considered as an alternative to hard disk drive (HDD) as the second storage device [START_REF] Margaglia | The Devil is in the Details: Implementing Flash Page Reuse with WOM Codes[END_REF]. With semiconductor process technology scaling and cell density improvement, the capacity of NAND flash memory has been increasing continuously and the price keeps dropping. However, technology scaling inevitably brings the continuous degradation of flash memory endurance and I/O performance, which motivates the search for methods to improve flash memory performance and lifetime [START_REF] Zhang | Reducing Solid-State Storage Device Write Stress Through Opportunistic In-Place Delta Compression[END_REF] [START_REF] Cui | Exploiting Latency Variation for Access Conflict Reduction of NAND Flash Memory[END_REF].

Flash lifetime, measured as the number of erasures a block can endure, is highly correlated with the raw bit error rate (RBER), which is defined as the number of corrupted bits per number of total bits read [START_REF] Schroeder | Flash Reliability in Production: The Expected and the Unexpected[END_REF]. As the endurance of flash cells is limited, RBER is expected to grow with the number of program/erase (P/E) cycles, and a page is deemed to reach its lifetime if the combined errors are not correctable by error correction code (ECC). Many methods have been proposed to maximize the number of P/E cycles in flash memory. They include enhancing the error correction capability of ECC [START_REF] Zhao | LDPC-in-SSD: making advanced error correction codes work effectively in solid state drives[END_REF] [6] [START_REF] Wu | Exploiting workload dynamics to improve SSD read latency via differentiated error correction codes[END_REF], distributing erasure costs evenly across the drives blocks [START_REF] Jimenez | Wear unleveling: improving NAND flash lifetime by balancing page endurance[END_REF] [9] [START_REF] Agrawal | Design Tradeoffs for SSD Performance[END_REF], and reducing the threshold voltages for less wearing incurred by each P/E cycling [START_REF] Jeong | Lifetime improvement of NAND flashbased storage systems using dynamic program and erase scaling[END_REF] [12] [START_REF] Jeong | Improving NAND Endurance by Dynamic Program and Erase Scaling[END_REF].

Flash read latency is also highly correlated with RBER. The higher the R-BER, the stronger the required ECC capability, as well as the higher the complexity of ECC scheme and the slower the read speed. Recently, several works have been proposed to reduce read latency by regulating the memory sensing precision. Zhao et al. [START_REF] Zhao | LDPC-in-SSD: making advanced error correction codes work effectively in solid state drives[END_REF] proposed the progressive soft-decision sensing strategy, which uses just-enough sensing precision for ECC decoding through a trial-anderror manner, to obviate unnecessary extra sensing latency. Cui et al. [START_REF] Cui | Exploiting Latency Variation for Access Conflict Reduction of NAND Flash Memory[END_REF] sorted the read requests according to the retention age of the data, and performed fast read for data with low retention ages by decreasing the number of sensing levels.

In this paper, the relationship among flash cell wearing, read latency and RBER is introduced. On one hand, flash cell wearing is reduced by lowering the threshold voltages but at the cost of less noise margins between the states of a flash cell, which in turn increase RBER and delay read operations. On the other hand, read latency can be decreased by improving the threshold voltages for lower RBER, which, however, results in more cell wearing. Based on the above relationship, we propose a comprehensive approach (HIRE) to exploit the access hotness information for improving read performance and endurance of flash memory storage systems. The basic idea is that we design a cross-layer hotness identifier in the buffer replacement management model of NAND flash memory, hence data pages in the buffer list can be classified into the following three groups, namely read-hot, write-hot and mixed-hot, respectively. Moreover, the fine-grained voltage controller is designed to supervise and control the appropriate threshold voltages of flash cells. In particular, the threshold voltages of a cell for write-hot data are decreased for wearing reduction, while these for read-hot data are increased for read latency reduction.

Trace-based simulations are carried out to demonstrate the effectiveness of our proposed approach. The results show that the proposed HIRE approach reduces the read response time by up to 43.49% on average and decreases the wearing of flash memory by up to 16.87% on average. In addition, HIRE does not have a negative write performance effect. Besides, the overhead of the proposed technique is negligible. In summary, this paper makes the following contributions.

• We proposed a cross-layer hotness identifier in the buffer replacement management model of NAND flash memory to guide flash read performance and endurance improvement. • We proposed a voltage controller in the flash controller to improve flashbased system performance metrics with the guidance of the proposed hotness identifier, which manages the appropriate threshold threshold voltages for three types of data (read-hot, write-hot, mixed-hot) evicted by the buffer replacement algorithm. • We carried out comprehensive experiments to demonstrate its effectiveness on both the wearing and read latency reduction without sacrificing write performance.

The rest of this paper is organized as follows. Section 2 presents the background and related work. Section 3 describes the design techniques and implementation issues of our hotness-guided access management for flash storage devices. Experiments and result analysis are presented in Section 4. Section 5 concludes this paper with a summary of our findings.

BACKGROUND AND RELATED WORK

In this section, we first present the tradeoff between flash cell wearing and read latency, which is due to two relationships. The first one is the relationship between threshold voltage, wearing and RBER. The second one is the relationship between error correction capability, read latency and the number of sensing levels when adopting LDPC as the default ECC scheme, which brings superior error correction capability as well as read response time degradation at the same time. Finally, previous studies related to this work are introduced for further work in this area.

Tradeoff between flash cell wearing and read latency

Firstly, the tradeoff between flash cell wearing and read latency is due to the relationship between threshold voltage, wearing and RBER. A flash chip is built from floating-gate cells whose state depends on the amount of charge they retain. Multi-level cell (MLC) flash memory uses cells with 4 or 8 states (2 or 3 bits per cell, respectively), as opposed to single-level cell (SLC) flash memory, which has 2 states (1 bit per cell). Every state is characterized by a threshold voltage (V th ), which can be changed by injecting different amounts of charge onto the floating-gate. Recently, several works have showed that flash cell wearing is proportional to the threshold voltages [START_REF] Jeong | Lifetime improvement of NAND flashbased storage systems using dynamic program and erase scaling[END_REF] [12] [START_REF] Pan | Exploiting Memory Device Wear-Out Dynamics to Improve NAND Flash Memory System Performance[END_REF]. The stress-induced damage in the tunnel oxide of a NAND flash memory cell can be reduced by decreasing the threshold voltages, and vice versa. Besides, the threshold voltages affect RBER significantly. When the threshold voltages are decreased, the noise margins among flash cell states are reduced, which reduces the capability for tolerating retention errors and increases RBER. Therefore, the tradeoff between wearing and RBER can be explored by controlling the threshold voltages with a wide range of settings. The less threshold voltages of a flash state, the less flash cell wearing, meanwhile, the higher RBER.

Secondly, the tradeoff is due to the significant relationship between error correction capability, read latency and the number of sensing levels when adopting LDPC scheme. The flash controller reads data from each cell by recursively applying several read reference voltages to the cell in a level-by-level manner to identify its threshold voltage. Therefore, sensing latency is linearly proportional to the number of sensing levels. In addition, when N sensing levels quantize the threshold voltage of each memory cell into N+1 regions, a unique log 2 (N + 1)bit number is used to represent each region, indicating that transferring latency is proportional to the logarithm of N+1. Although read requests are delayed by slower sensing and transferring when using more sensing levels, more accurate input probability information of each bit for LDPC code decoding can be obtained, thus improving error correction capability (CBER).

Based on the precondition that RBER should be within CBER of the deployed LDPC code, the tradeoff between flash cell wearing and read latency can be concluded from above two relationships. As shown in Figure 1, flash cell wearing can be reduced by lowering the threshold voltages but at the cost of less noise margins between the states of a flash cell, which in turn increase RBER and delay read operations.

Related Work

Several methods for improving NAND flash memory I/O performance and endurance have been suggested by exploiting either of the two described relationships. By tasking advantage of the relationship between threshold voltage, wearing and RBER, Peleato et al. [START_REF] Peleato | Maximizing MLC NAND lifetime and reliability in the presence of write noise[END_REF] proposed to optimize the target voltage levels to achieve a trade-off between lifetime and reliability, which tried to maximize lifetime subject to reliability constraints, and vice versa. Jeong et al. [START_REF] Jeong | Lifetime improvement of NAND flashbased storage systems using dynamic program and erase scaling[END_REF] presented a new system-level approach called dynamic program and erase scaling to improve the NAND endurance, by exploiting idle times between consecutive write requests to shorten the width of threshold voltage distributions so that blocks can be slowly erased with a lower erase voltage. However, both of them would induce the negative effects such as increased error and decreased write throughput.

Another set of approaches takes the relationship between error correction capability, read latency and the number of sensing levels into account. For example, Zhao et al. [START_REF] Zhao | LDPC-in-SSD: making advanced error correction codes work effectively in solid state drives[END_REF] proposed the progressive sensing level strategy to achieve latency reduction, which uses soft-decision sensing only triggered after the hard-decision decoding failure. Cai et al. [START_REF] Schroeder | Flash Reliability in Production: The Expected and the Unexpected[END_REF] presented a retention optimized reading (ROR) method that periodically learns a tight upper bound and applies the optimal read reference voltage for each ash memory block online. Cui et al. [START_REF] Cui | Exploiting Latency Variation for Access Conflict Reduction of NAND Flash Memory[END_REF] sorted the read requests according to the retention age of the data, and performed fast read for data with low retention ages by decreasing the number of sensing levels. These state-of-the-art retention-aware methods improve the read performance significantly, and fortunately they are orthogonal to our work.

These studies demonstrate that wearing reduction by adjusting voltage and read performance improvement by soft-decision memory sensing are useful. However, none of these works consider the tradeoff between read latency and wearing when exploiting both of the two described relationships. In this paper, we focus on reducing both the read latency and wearing by controlling the threshold voltages based on the hotness information of each request, which can be easily acquired from the buffer manager.

Exploiting Cross-Layer Hotness Identification to

Improve Read and Endurance Performance (HIRE)

In this section, we propose HIRE, a wearing and read reduction approach, which includes two new management strategies: Hotness Identifier (HI) captures the access hotness characteristics at the flash buffer management level and Voltage Controller (VC) modulates the appropriate threshold voltages of a flash cell. We first present the cross-layer study on the access hotness characteristics of each data page in several workloads based on the buffer replacement policy. Then, on the basis of the observations of this cross-layer study, we propose a hotnessguided voltage controller to reduce the wearing and read latency. Finally, we present the overhead analysis.

Cross-Layer Study for Hotness Identifier

In order to guide wearing and read latency reduction, the access hotness characteristics of each data page are needed. The hotness in this work means the frequency of read or write operations on each data page for a given period of time. We find that the hotness characteristics can be archived by the buffer manager. Buffer replacement policy can optimize the I/O sequence and reduce storage accesses, thus improving the overall efficiency of the storage system. In this study, we use the simple and efficient Least Recently Used (LRU) policy to acquire these information. Note that other buffer replacement algorithms for NAND flash-based storage systems, e.g., PT-LRU [START_REF] Cui | PT-LRU: a probabilistic page replacement algorithm for NAND flash-based consumer electronics[END_REF] or HA-LRU [START_REF] Lin | History-aware page replacement algorithm for NAND flash-based consumer electronics[END_REF], are completely orthogonal to our work, and can be also used with the proposed HIRE approach to improve flash-based system performance metrics. We implement the Hotness Identifier (HI) strategy in the buffer manager. LRU uses a linked list to manage all cached data page, and when data page is evicted out of the buffer, the historical statistical information about the read/write hit can be used to identify the access hotness characteristics because the read/write hit statistical information reflect the access history. In order to collect the access hotness characteristics, each data page in the buffer list adds two attributes: buffer read hit count C r and buffer write hit count C w . If one data page is first referenced, it will be added into the MRU position of the buffer linked list, besides, its corresponding buffer read/write hit value will plus one according to its read/write operation, respectively. When the data page in the buffer is referenced again, LRU adjusts the position of the data page to the MRU position of the linked list, meanwhile, its corresponding buffer read/write hit count value will also plus one according to its read/write operation.

During the eviction procedure, we classify the data access characteristics in the buffer into three types, as shown in Figure 2. When the buffer does not have a free page slot for the new access data, LRU preferentially evicts the data page in the LRU position of the linked list, which is the least recently accessed data page. At this time, when the read hit ratio grows to a high watermark Cr Cr+Cw > w (in this work w = 95%), the most hit statistical information of a data page are read, and we determine it as read-hot (RH). For instance, the request data pages in the WebSearch trace from a popular search engine [START_REF]Storage Performance Council traces[END_REF] are all read only, therefore, all data pages in this trace will be identified as RH. When the write hit ratio grows to a high watermark Cw Cr+Cw > w, the most hit statistical information of a data page are write, and we determine it as write-hot (WH). Hence, other pages mixed with read and write hit are identified as mixed-hot (MH). As a result, data page are classified into three groups according to their access hotness characteristics.

Voltage Controller in HIRE

Based on the access hotness characteristics of each data page, the Voltage Controller (VC) strategy, aiming to the wearing and read latency reduction, is proposed, as shown in Figure 2. Furthermore, blocks transition between five states are used in this work to cooperate with the fine-grained voltage controller strategy, namely clean, readActive, writeActive, mixActive and used. Clean state is an initial state of a block which receives none program operation, or is erased.

To improve the read performance, VC implemented in the flash controller boosts the threshold voltages of flash cells that store RH data, and hence the noise margins between the states of a flash cell increase, increasing the wearing of flash memory, but it leads to lower raw bit error rates so that its read performance is further improved. Note that RH data defines the resources stored in RH data page. Moreover, VC performs this RH data on a block with readActive state. If there is no readActive block, a block with clean state will be chosen as the current readActive block. When all pages on the readActive block have been written, it moves to the used state, and a new readActive block will be produced by the above method. Note that although the wearing is estimated to somewhat higher than that of the horizontal voltage line, fewer P/E (Program/Erase) operations in this read-hot data compensates for the wearing increment. Thus, this relatively small increment of wearing is acceptable to achieve the read performance improvement in the read-hot data.

If one data is classified as WH, the threshold voltages of corresponding flash cells are reduced, which reduces the wearing of flash memory. Simultaneously, VC performs this data on a block with writeActive state. When all pages on the writeActive block have been written, this block also moves to the used state, and a new clean block will be chosen as the current writeActive block. Although RBER is consequently higher in WH, the number of errors within a code word is not beyond the superior error correction capability of LDPC code. Moreover, the corresponding block is more likely to trigger garbage collection (GC) because of the write-hot access characteristic.

Traditional voltage control without the fluctuation of threshold voltages, is applied in MH data. These MH data will be performed on a block with mixActive state. When all pages on the mixActive block have been written, it also moves to the used state, and VC will chose a clean block as the current mixActive block. And when a used block is chosen by GC, it will be erased and move back to the clean state. Similar to hot/cold data separation policy [START_REF] Jung | A process-aware hot/cold identification scheme for flash memory storage systems[END_REF] [23], separating readActive, writeActive and mixActive blocks improves the efficiency of garbage collection.

Overhead Analysis

The implementation of the proposed HIRE approach includes method implemented in the flash buffer manager and information recorded in the flash controller. In the flash buffer manager, we need to maintain the access hotness information. In order to figure out these information, the buffer list adds two attributes, including buffer read and write hit counts. We assume that the most buffer hit read/write counts is N h , and the buffer size is N c which specifies the maximum number of pages cached by buffer pool in this work, then the maximal size of storage required by the access hotness information is log 2 N h × 2 × N c bits. This storage overhead is negligible for a state-of-the-art SSD. In addition, we also extend each mapping entry in the flash translation layer of flash controller with a hotness field, using 2 bits to record three types of access hotness (RH, WH and MH ), which is also negligible for a state-of-the-art SSD. Thus, it can be seen that the storage overhead is negligible.

Performance Evaluation

In this section, we first present the experimental methodology. Then, the I/O performance and endurance improvement of the proposed voltage optimization are presented. For comparison purpose, we have implemented several works which are closely related to our proposed HIRE approach.

Methodology

In this paper, we use an event-driven simulator to further demonstrate the effectiveness of the proposed HIRE. We simulate a 128GB SSD with 8 channels, each of which is connected to 8 flash memory chips. We implement dynamic page mapping scheme between logical and physical locations as the FTL mapping scheme. Greedy garbage collection and dynamic wear-leveling scheme are also implemented in the FTL of the simulator. All these settings are consistent with previous works [START_REF] Cui | Exploiting Latency Variation for Access Conflict Reduction of NAND Flash Memory[END_REF]. As shown in Table 1, under the traditional voltage control, (1.17, 2.37, 2.96, 3.54) represents the threshold voltage of the four states in the simulated 2 bit/cell MLC NAND flash memory chip, and we use 600 µs as the program latency when ∆V p is 0.25, 90 µs as memory sensing latency and 80 µs as data transfer latency when using LDPC with seven reference voltages. For the boosted threshold voltages, (1.40, 2.85, 3.55, 4.25) represents the corresponding threshold voltage of the four flash cell states when ∆V p is 0.3, 30 µs as memory sensing latency and 40 µs as data transfer latency. When the threshold voltages reduce, the threshold voltage of four flash cell states is (0.93, 1.90, 2.37, 2.83) and ∆V p is 0.2, the sensing latency is 210 µs and the data transfer latency is 100 µs.

For validation, we implement HIRE as well as baseline, HVC and LVC. We treat traditional voltage control strategy without any further targeted optimization as the baseline case in our contrastive experiments. HVC (High Voltage Controller) approach increases threshold voltages of all flash cells to maximize read latency reduction, while LVC (Low Voltage Controller) approach reduces threshold voltages of all the flash cells to maximize wearing reduction. We evaluate our design using real world workloads from the MSR Cambridge traces [START_REF] Narayanan | Migrating server storage to SSDs: Analysis of tradeoffs[END_REF] and two financial workloads [START_REF]Storage Performance Council traces[END_REF], which are widely used in previous works to study SSD system performance metrics [19] [20] [21].

Experiment Results

In this section, the experimental results are presented and analyzed. Seventeen datasets were used in the experiments including a variety of application scenarios. To test the performance of our approach, the I/O response time and wearing are presented below.

Figure 3 shows the read latency of the proposed HIRE under different datasets, as compared to baseline, HVC and LVC approaches. It can be seen that HIRE outperforms baseline under all datasets, reducing read latency by 43.49% on average. From Figure 3, we can also see that the read performance improvement of HIRE under different datasets is distinctly different. For the stg1 trace, the percent read latency reduction between baseline and HIRE is 58.59%. For the fin1 trace, the percent read latency reduction between baseline and HIRE is 6.89%. HIRE increases voltages for the read-hot data, thus more read-hot significantly reduces the read latency. Figure 3 also shows that HVC approach archives the maximize read performance improvement, which is even better than HIRE. This significant improvement achieved for HVC approach is attributed to the fact that persistently increasing voltages leads to the minimize read response time, while HIRE only increases voltages of the read-hot data. However, HVC will also get the worst flash wearing at the same time, which can be seen in Figure 4.

Figure 4 shows the wearing weight for the seventeen traces under four approaches. Wearing weight is invoked as the metric to show the wearing degree of the proposed approach. The lower wearing weight, the longer endurance of storage system. It can be seen that compared with the traditional baseline approach, HIRE achieves significant wearing reduction. HIRE outperforms baseline with wearing reduction by 16.87% on average. On the other hand, compared to baseline, the greatest wearing reduction observed in stg1 is 19.99%, while the smallest reduction observed in fin2 is only 1.66%. This is because HIRE drops voltages for the write-hot data, thus more write-hot data significantly reduces the wearing. Moreover, HVC gets the maximum wearing weight although it realizes the maximum read latency reduction, which has been discussed above.

To further demonstrate that our HIRE approach does not sacrifice the write performance, the normalized write latency in all experiments are measured and presented in Figure 5. It can be seen that, very intuitively, the write latency of HIRE is comparable to those of the three competitor approaches. We can thus get the conclusion that the voltage control strategy in the proposed HIRE approach does not affect the write latency of the storage system.

Conclusion

In this paper, we proposed HIRE, a wearing and read reduction approach, that applies two new management strategies in NAND flash memory storage system: Hotness Identifier (HI) captures the hotness characteristics at the flash buffer management level and Voltage Controller (VC) manages the appropriate threshold voltages of a flash cell in the flash controller. The key insight behind the design of HIRE is that based on the access hotness characteristics provided by HI, VR decreases the threshold voltages of a flash cell for the write-hot data for wearing reduction and increases these for the read-hot data for read latency reduction. Extensive experimental results and detailed comparisons show that the proposed approach is effective in various types of workloads for NAND flash memory storage system. On average, HIRE improves read performance by up to 43.49% and decreases the wearing of flash memory by up to 16.87% over previous voltage management approaches. In addition, HIRE does not have a negative write performance effect, and the overhead of the proposed approach is negligible.

Fig. 1 .

 1 Fig. 1. Relationship between flash cell wearing and read latency.

Fig. 3 .

 3 Fig. 3. The read latency under different voltage control approaches.

Fig. 4 .Fig. 5 .

 45 Fig. 4. The wearing weight under four approaches.

Table 1 .

 1 Parameters in this work

	T hreshold V oltages	Sensing (µs)	Transfer (µs)	Program (µs)
	(1.40, 2.85, 3.55, 4.25)	30	40	600
	(1.17, 2.37, 2.96, 3.54)	90	80	600
	(0.93, 1.90, 2.37, 2.83)	210	100	600

Acknowledgment

The authors would like to thank the anonymous reviewers for their detailed and thoughtful feedback which improved the quality of this paper significantly. This work was supported in part by the National Natural Science Foundation of China under grant NO.91330117, the National High-tech R&D Program of China (863 Program) under grant No.2014AA01A302, the Shaanxi Social Development of Science and Technology Research Project under grant No. 2016SF-428, the Shenzhen Scientific Plan under grant No.JCYJ20130401095947230 and No.JSGG20140519141854753.


Peng Qu

Jin Yan

Guang R Gao

Toward A Parallel Turing Machine Model

Keywords: Parallel Turing Machine, Codelet, Abstract Architecture, Parallel Computing

In the field of parallel computing, the late leader Ken Kennedy, has raised a concern in early 1990s: "Is Parallel Computing Dead?" Now, we have witnessed the tremendous momentum of the "second spring" of parallel computing in recent years. But, what lesson should we learn from the history of parallel computing when we are walking out from the bottom state of the field? To this end, this paper examines the disappointing state of the work in parallel Turing machine models in the past 50 years of parallel computing research. Lacking a solid yet intuitive parallel Turing machine model will continue to be a serious challenge. Our paper presents an attempt to address this challenge -by presenting a proposal of a parallel Turing machine model -the PTM model. We also discuss why we start our work in this paper from a parallel Turing machine model instead of other choices.

Introduction & Motivation

Parallel computing is a type of computation in which many calculations are carried out simultaneously, operating on the principle that large problems can often be divided into multiple smaller ones such that teamwork by multiple processors can deliver the computational result sooner.

Historically, we have witnessed significant progress in parallel computing from 1960s to 1980s. Notable advances in parallel computer architecture have been made ranging from the R&D on massive SIMD parallel computers [START_REF] Bouknight | The Illiac IV system[END_REF] to the vector processing computers. However, in the early 1990s, the once bright looking future of the parallel and high-performance computing field had encountered serious challenge -so serious that had prompted a well known speech entitled "Is Parallel Computing Dead?" [START_REF] Kennedy | Is parallel computing dead?[END_REF] given by late Ken Kennedy -an influential world leader of parallel computer field in 1994.

In the meantime, the world has witnessed the fantastically successful history of sequential computer systems based on so-called von Neumann model. The first von Neumann machine EDVAC [START_REF] Eckert | Automatic high-speed computing: a progress report on the EDVAC[END_REF] based on von Neumann architecture [START_REF] Von Neumann | First Draft of a Report on the EDVAC[END_REF] was proposed in 1946 and soon found significant commercialization opportunities. Why does von Neumann architecture (the sequential computer architecture as it has been known) have such a robust history for over the past 60 plus years and continue to flourish in many ways into the new millennium? why does sequential approach continue more successfully than the parallel, given the advantages of the parallel approach?

One of such pillars is a robust sequential programming model whose foundation is based on the Turing machine model and the von Neumann architecture model that specifies an abstract machine architecture to efficiently support the Turing machine model. What should be the equivalent pillar to support parallel computation?

Unfortunately, there is no commonly accepted parallel Turing machine model and a corresponding parallel abstract architecture model for its realization. However, much good work on parallel models of computation exist, such as Leslie G. Valiant's work, proposing the Bulk Synchronous Parallelism (BSP) model as a bridging model of parallel computation between hardware and software [START_REF] Valiant | A bridging model for parallel computation[END_REF], and David Culler's work on the LogP model as a practical model of parallel computation which focuses on performance characterization of parallel algorithms [START_REF] Culler | LogP: A practical model of parallel computation[END_REF] -both served as significant milestones in the path searching for good models of parallel computation.

Most of the popular work on parallel models of computation have their basis on the concept of threads. Threads are a seemingly straightforward adaption of the dominate sequential model of computation in concurrent systems. However, as Ed. Lee stated in his paper "The Problem with Threads", "they discard the most essential and appealing properties of sequential computation: understandability, predictability and determinism." [START_REF] Lee | The problem with threads[END_REF] Consequently, in this paper, we choose to begin our work from a Turing machine model -in a path that is not actively pursued in prior research of parallel models of computation. We believe that there is a need to clearly identify the two corner stones of a parallel Turing machine model: a parallel program execution model (PXM) and an abstract architecture model. The sound properties of parallel programs should be specified in a clean and simple program execution model (PXM), which is not based on threads, while the realization of PXM should be the role of the design of an efficient abstract architecture modeland there may well be more than one design choice.

A summary of main contributions of this paper is outlined as follows:

-A survey reveals a disappointing status of the field of parallel Wiederman generalized Hemmerling's model [START_REF] Wiedermann | Parallel Turing machines[END_REF] in an article published in 1984. Wiederman's parallel Turing machine has one infinite tape, as does a sequential Turing machine, but it may have multiple processing units (PUs), namely multiple read/write heads. Each processing unit, working in a similar fashion as a single sequential Turing machine, can read the input from the tape and write the output back to the tape independently. Figure 1a illustrates Wiederman's model.

The behavior of a "program", namely the corresponding FSM of a parallel Turing machine, is quite different from that of sequential Turing machine. Consider a state S of a FSM that has several successor states {S1, S2,. . . } all corresponding to the same input. Under a sequential Turing machine, the transition from S will non-determistically select one of the states from the set {S1, S2,. . . } to be next state and make a transition accordingly. Under Wiederman's Turing machine model, state S makes transitions to a set of states {S1,S2,. . . } simultaneously, as shown in Figure 1b.

Wiederman's model starts with a single processing unit; as soon as the computation begins, when a running processing unit (PU) encounters any state with multiple succeeding states labelled with the same input, the FSM will begin to exploit the power of parallelism dynamically, i.e., the processing unit (PU) will Generating the new processing units: PU0 copies itself yielding PU1 and PU2, each with its own event in the shared FSM control produce copies of itself, so that there is one PU for each of the possible transitions, and carries out the operations.

1 1 0 0 1 …. S0 S1 S2 Si PU1 PU2 1 S3 1 0 Control FSM (a) 0 1 1 0 1 PU0 …. S0 S1 S2 Si 1 S3 1 0 Control FSM PU2 PU1 (b)
Figure 1b and 1a illustrate this situation. In figure 1b, PU0 whose state is in S0 meets symbol '1'. Sharing the contol FSM, it provides for two processing units (PU1 and PU2) with events for state S1 and S2 respectively. After the multiplication, each of these processing units works as a separate Turing machine. However, all the new processing units in Wiederman's parallel Turing machine will still share the same FSM which is the same with the FSM before multiplying, as shown in figure 1a. The only difference between these PUs is that they are in different states of the FSM -the green PU1 is in state S1 and the brown PU2 is in state S2.

From our reading, in Wiederman's model, it appears to follow an assumption that all PUs run synchronously, which means they all finish a step in the same time. Thus additional wait states may be used to avoid serious conflicts (i.e., two memory operations happen concurrently and at least one of them is a write). However, if we allow the PUs to operate asynchronously, serious conflict, such as reordering writes to be after VS. before reads, may occur.

The disappointing status on parallel Turing machine studies

There is little published work on parallel Turing machine. The few parallel Turing machine proposals we are aware of still use tapes as the model of storage in the corresponding architecture description. There seems to be little enthusiasm for or interest in searching for a commonly accepted parallel Turing machine model and corresponding abstract architecture model in the field of parallel computing. This is true even during the past 10+ years of the second spring of parallel computing.

Forty years have passed since Hemmerling's attempt to propose a parallel Turing machine model in 1979. In Computer Science, the field of concurrency -which covers both parallel computing and distributed computing -has advanced significantly since its infancy in 1960s and early 70s [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF]. With the experience and lessons of the serious down turn of parallel computing in the 1990s, we also learned the importance of developing a standard, robust interface between software and hardware as a basis of machine independent parallel programming.

Today, any serious attempts on parallel Turing machine must have a solid model of memory beyond Turing's tape storage. As described in previous section on Wiederman's model, after the multiplication, those replicated processing units will operate in parallel but they still work on the same tape. So they will communicate with each other by reading and writing a shared memory location. However, concurrent access of the shared memory location may cause a conflict. The resolution of such memory conflicts must deal with the so-called memory consistency model of the underlied architecture model -a field pioneered by Leslie Lamport in 1978 [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] -at about the same time as the first parallel Turing machine work by Hemmerling was published.

A Parallel Turing Machine Model -Our Proposal

Like we have mentioned earlier, we choose to start our work on a parallel Turing machine model, instead of following the research of parallel models of computation. Section 3.1 gives a definition and description of concepts of codelets and codelet graphs. Section 3.2 demonstrates our proposed PTM, consisting of a PXM and an abstract architecture, while section 3.3 shows an example of how the PTM works. Finally, in section 3.4, we have a short discussion of determinacy property of our proposed PTM.

The concept of codelets and codelet graphs (CDGs)

Codelets A codelet is a unit of computation that can be scheduled atomically for execution and it is the principal scheduling quantum (PSU) in codelet based execution model. A codelet may be made up of a group of (many) machine level instructions and organized with various control structures including loops. Once become enabled (i.e. ready to be scheduled for execution), a codelet may be scheduled to an execution unit (or EU) and be executed non-preemptively as an atomic PSU -keeping the EU usefully busy until its termination. The effectiveness of the non-preemptive model has been demonstrated through the mapping of a number of applications onto a many-core chip architecture with 160 cores [START_REF] Garcia | Energy efficient tiling on a Many-Core Architecture[END_REF].

Codelet graphs A program can be organized by a composition of multiple codelets into a graph called a codelet graph. A CDG is a directed graph G(V, E), where V is a set of nodes and E is a set of directed arcs. In a CDG, nodes in V may be connected by arcs in E. Every node in G denotes a codelet.

An arc (V 1 , V 2 ) in the CDG is a representation of a precedence relation between nodes V 1 and V 2 . Such a relation may be due to a data dependence between codelet V 1 and V 2 .

The concept of a codelet graph (CDG) has its origin in dataflow graphs [START_REF] Dennis | Data flow schemas[END_REF]. In particular, it leverages the dataflow program graphs proposed in the McGill Dataflow Architecture Model [START_REF] Gao | An efficient hybrid dataflow architecture model[END_REF]. Consequently, a unique feature of CDGs is that they employ the "argument-fetching " dataflow model proposed by Dennis and Gao [START_REF] Dennis | An efficient pipelined dataflow processor architecture[END_REF][START_REF] Gao | Design of an efficient dataflow architecture without data flow[END_REF].

Firing rules The execution model of a codelet graph is specified by its operational semantics -called firing rules: A codelet that has received all the required events -"signal tokens" on the corresponding input arcs of the codelet -will become enabled. Any enabled codelet can be scheduled for execution (or called "firing", a term used in dataflow models of computation). Firing of an enabled codelet will consume all the input events (remove the signal tokens), perform the computation as specified by the codelet and produce results, and generate output events.

The Parallel Turing machine model

Program execution model (PXM) of the PTM

In our model, a PTM consists of a codelet graph (CDG) and a memory. The CDG can execute a program, which has been described in section 3.1. It serves as the function of a "program" just like the finite state machine (FSM) in sequential Turing machine. A memory consists of a set of locations. The content of each location is addressable by an addressing mechanism, and manipulated through a set of memory operations like load and store operations. For the purpose of this paper, the memory can be considered organized and operated as a RAM (random access memory). The memory organization itself is left to be defined by a specific abstract architecture model and will be discussed later. A state of a PTM consists of the state of the CDG and memory. At a particular time, a state of a CDG is its configuration at that time, while the state of memory is the content of the memory at that time. A configuration of CDG is the assignment of events on the arcs of the CDG. An initial state of the PTM is the initial configuraton of the CDG and the initial contents of the memory. The computation of a PTM is carried out by the state transitions defined as follows.

Assume the CDG is currently at a particular state. Based on the current configuration, there may be a set of codelets which are enabled (or in enable state) and a subset of which is selected to fire. Firing of an enabled codelet consists of the following three steps: firstly, it consumes all the input events; then the processing unit will read the input data from memory, perform the computation as specified by the codelet; finally, it stores results into memory,

The term token, is from a familiar terminology of dataflow literature. In the rest of this paper, we use the term events to denote signal tokens (or event tokens) present on certain arcs. and generates output events. When the computation (firing) of the codelet is completed, some new events will be produced, and placed on its corresponding output arcs according to the specific firing rule of it. Also, upon completion, the memory state will be updated. Upon the completion of the firing of all selected codelets, a new state of the PTM is reached -consisting of a new configuration and a new memory state. This will complete the state transition process. An abstract architecture model of the PTM Now, we present the abstract architecture model of our proposed PTM which we named as CAM -i.e., codelet abstract machine, as shown in figure 2.

A CAM consists of (1) a collection of codelet processing units (CPUs) and memory units (MUs), (2) a collection of codelet scheduling units (CSUs), (3) a hierarchy of interconnection network (HIN). The CPUs and MUs can be grouped together by connecting through the HIN and form nodes of the CAM. A number of nodes can be connected into a cluster through the HIN. These clusters can be further connected and organized into higher-level hierarchy such as a hierarchy of trees, meshes, etc. The MUs in CAM are organized to share a single shared address space. Consequently, the design decision on the memory consistency model is critical. Our PTM and its CAM will follow a specific memory consistency model. However, the details of the memory consistency model (MCM) and the structure of clusters connected by HIN are left as a design decision for any particular physical architecture that realizes the CAM. That is, we assume any physical architecture that implements the CAM will make the choice of a specific MCM and cluster structure that best apply to the underlying programming environment, hardware technology and other trade-offs so that a physical architecture and related machines may be built. Note that our CAM follows the stored-program principle as described by John von Neumann in the description of the EDVAC machine [START_REF] Von Neumann | First Draft of a Report on the EDVAC[END_REF]. However, our CAM design may eliminate one-word-at-a-time be-tween CPU and memory by permitting multiple data words be communicated concurrently between memory (made of multiple memory units) and CPUs.

An example to illustrate how the PTM works

In figure 3 we illustrate a simple but informative CDG example of the proposed Parallel Turing machine. This "program" will first invert the tape contents and then change all the contents to '0'. If there are many execution units to do the work, which means each processing unit does the invert operation or changes the symbol to '0' at a specific memory location, the total excution time should be much less. Codelet A (figure 3a) is a compound codelet which does the invert operation. It is defined as a conditional schema consisting of a decider, two codelets and a conditional merge. Codelet A is enabled once the input event (a) is available on the input arc. When fired, it will invert the content of memory location a. Also, an output event will be generated. Codelet B (figure 3b) is a simple codelet. It is enabled whenever the input event (a) arrives. When fired, it changes the content of memory location a to '0' and generates the output event.

A M[a]==1? T F T F M[a]=0 M[a]=1 b a (a) M[a]=0 a event B (b)
Figure 3c illustrates a non-conflict CDG, which does exactly what we need and exploits as much parallelism as is presented in the problem to be solved. The three codelet As in figure 3c are first enabled by inputs and their outputs will carry the value of memory locations to be accessed and enable three codelet Bs. The numbers 0, 1 and 2 on codelet As' input arcs, act as the values of memory locations to be accessed. It means that when the input events arrive, the left codelet A, the middle codelet A and the right codelet A will invert the content of memory location 0, 1, 2 separately. So the contents of all the involved memory locations will be first inverted and then changed to '0'.

Figure 4 gives a detailed description about how the CDG is executed. A CDG could be executed on a CAM with arbitrary number of CPUs. Take figure 4 as an example. If there are more than three CPUs, three codelet As could be executed by any three of them. If there are fewer than three CPUs, the parallelism can not be fully exploited, only some of the enabled codelets (usually the same number as there are idle CPUs) are chosen by the CSUs and are executed first, then the CSUs continuously choose enabled codelets to execute until there are no more enabled codelets. Without losing generalization, we use a CAM with three CPUs to explain how this CDG is executed. 1.

Step 1, the input events reach the corresponding input arcs of codelet As, thus all the codelet As are enabled. 2. Step 2, as there are three CPUs, the same number with enabled codelets, all these enabled codelet As are fired. They consume all the input events, invert the content of memory locations 0, 1 and 2, and then generate output events respectively. These output events further reach codelet Bs' input arcs, thus all three codelet Bs are enabled.

3.

Step 3, all the enabled codelet Bs are fired. They consume all the input events, change the content of memory locations 0, 1 and 2 to '0' and then generate output events respectively. 4.

Step 4, all those enabled codelets are fired and no more enabled codelets left, now the computation is finished.

If there are enough units (say, six), we can change the CDG to let all these six codelets enabled at the same time to achieve significant speedup. Although this may cause conflicts when several codelets which have data dependence are scheduled at the same time, we could use a weak memory consistency model to avoid it.

From the previous examples, we can see that our proposed PTM has advantages over Wiederman's model: using event-driven CDG, we can illustrate a parallel algorithm more explicitly. What's more, since necessary data dependence is explicitly satisfied by the "events", our PTM could execute a CDG correctly regardless of the number of CPUs or whether they are synchronous or not. Meanwhile, using memory model to replace Turing tape, as well as CAM instead of read/write head, we make it more suitable to realize our PTM in modern parallel hardware design. Thus, we still leave enough design space for system architecture and physical architecture design. For example, we don't limit the design choices of the detailed memory consistency model and cluster structure, because these design choices may differ according to the specific application or hardware.

Determinacy property of our proposed PTM

Jack Dennis has proposed a set of principles for modular software construction and described a parallel program execution model based on functional programming that satisfied these principles [START_REF] Dennis | A parallel program execution model supporting modular software construction[END_REF]. The target architecture -the Fresh Breeze architecture [START_REF] Dennis | Fresh Breeze: a multiprocessor chip architecture guided by modular programming principles[END_REF] -will ensure a correct and efficient realization of the program execution model.

Several principles of modular software construction, like Information-Hiding, Invariant Behavior, Secure Argument and Recursive Construction principle are associated with the concept of determinacy [START_REF] Dennis | Programming semantics for multiprogrammed computations[END_REF]. Consequently, the execution model of our proposed PTM laid the foundation to construct well-behaved codelet graphs which preserve the determinacy property. A more detailed discussion of the well-behaved property and how to derive a well-behaved codelet graph (CDG) from a set of well-structured construction rules have been outlined in [START_REF] Gao | Toward an execution model for extremescale systems-runnemede and beyond[END_REF], where the property of determinacy for such a CDG is also discussed.

Related Work

Parallel Turing machine

There seems to be little enthusiasm for or interest in searching for a commonly accepted parallel Turing machine model. This is true even during the past 10+ years of the second spring of parallel computing.

In section 2, we have already introduced the early work on parallel Turing machine models proposed by Hemmerling and Wiederman. Wiederman showed that his parallel Turing machine was neither in the "first" machine class [START_REF] Van Emde Boas | Machine models and simulations[END_REF], which is polynomial-time and linear-space equivalent to a sequential Turing machine, nor in the "second" machine class, which cannot be simulated by STM in polynomial time.

Since the publication of early work on parallel Turing machine models, some researchers have investigated different versions of these parallel Turing machine models. Ito [START_REF] Ito | Synchronized alternation and parallelism for three-dimensional automata[END_REF] and Okinakaz [START_REF] Okinaka | A note on hardware-bounded parallel Turing machines[END_REF] analyzed two and three-dimensional parallel Turing machine models. Ito [START_REF] Ito | Parallel Turing machines on fourdimensional input tapes[END_REF] also proposed a four-dimensional parallel Turing machine model and analyzed its properties. However, these works focused on extending the dimension of parallel Turing machine model of Wiederman's work, but ignore its inherent weaknesses outlined at the end of Section 2.

Memory consistency models

The most commonly used memory consistency model is Leslie Lamport's sequential consistency (SC) model proposed in 1978 [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF]. Since then, numerous work have been conducted in the past several decades trying to improve SC model -in particular to overcome its limitation in exploitation of parallelism. Several weak memory consistency models have been introduced, including weak consistency (WC, also called weak ordering or WO) [START_REF] Dubois | Memory access buffering in multiprocessors[END_REF] and release consistency (RC) [START_REF] Gharachorloo | Memory consistency and event ordering in scalable shared-memory multiprocessors[END_REF] models.

Existing memory models and cache consistency protocols assume memory coherence property which requires that all processors observe the same order of write operations to the same location [START_REF] Gharachorloo | Memory consistency and event ordering in scalable shared-memory multiprocessors[END_REF]. Gao and Sarkar have proposed a new memory model which does not rely on the memory coherence assumption, called Location Consistency (LC) [START_REF] Gao | Location consistency -a new memory model and cache consistency protocol[END_REF]. They also described a new multiprocessor cache consistency protocol based on the LC memory model. The performance potential of LC-based cache protocols has been demonstrated through software-controlled cache implementation on some real world parallel architectures [START_REF] Chen | A study of a software cache implementation of the openmp memory model for multicore and manycore architectures[END_REF].

The codelet model

The codelet execution model [START_REF] Gao | Toward an execution model for extremescale systems-runnemede and beyond[END_REF] is a hybrid model that incorporates the advantages of macro-dataflow [START_REF] Gao | Towards an efficient hybrid dataflow architecture model[END_REF][START_REF] Iannucci | Toward a dataflow/von Neumann hybrid architecture[END_REF] and von Neumann model. The codelet execution model can be used to describe programs in massive parallel systems, including hierarchical or heterogeneous systems.

The work on codelet based program execution models has its root in early work of dataflow models at MIT [START_REF] Dennis | First version of a data flow procedure language[END_REF] and elsewhere in 1960-70s. It was inspired by the MIT dynamic dataflow projects based on the tagged-token dataflow model [START_REF] Arvind | Executing a program on the MIT tagged-token dataflow architecture[END_REF] and the MIT CILK project [START_REF] Blumofe | Cilk: An efficient multithreaded runtime system[END_REF] of Prof. Leiserson and his group. The codelet execution model extends traditional macro-dataflow models by adapting the "argument-fetching" dataflow model of Dennis and Gao [START_REF] Dennis | An efficient pipelined dataflow processor architecture[END_REF]. The term "codelet" was chosen by Gao and his associates to describe the concepts presented earlier in Section 3.1. It derives from the concept of "fiber" proposed in early 1990s in EARTH project [START_REF] Humy | A design study of the EARTH multiprocessor[END_REF] which has been influenced strongly by the MIT Static Dataflow Architecture model [START_REF] Dennis | A preliminary architecture for a basic data-flow computer[END_REF]. As a result, we can employ a popular RISC architecture as a codelet execution unit (PU) [START_REF] Hennessy | Computer architecture: a quantitative approach[END_REF].

The terminology of codelet under the context of this paper was first suggested by Gao, and appeared in a sequence of project notes in 2009-2010, that finally appeared in [START_REF] Gao | Toward an execution model for extremescale systems-runnemede and beyond[END_REF]. It has been adopted by a number of researchers and practitioners in the parallel computing field. For example, the work at MIT led by Jack Dennis -the Fresh Breeze project, the DART project at university of Delaware [START_REF] Gao | Toward an execution model for extremescale systems-runnemede and beyond[END_REF], and the SWift Adaptive Runtime Machine (SWARM) under the DOE Dynax project led by ETI [START_REF] Lauderdale | Position paper: Towards a codelet-based runtime for exascale computing[END_REF]. The DOE Exascale TG Project led by Intel has been conducting research in OCR (Open Community Runtime) which is led by Rice University [START_REF] Mattson | OCR: The open community runtime interface version 1[END_REF]. And the relation between OCR and the above codelet concept can be analysed from [START_REF] Zuckerman | Using a codelet program execution model for exascale machines: position paper[END_REF]. What also notable to this community is the recent R&D work pursued at DOE PNNL that has generated novel and promising results.

Work on parallel computation models

In Section 1, we already include a discussion of related work on parallel computation models. For space reasons, we will not discuss these works further. However, we still wish to point out some seminal work following modular software engineering principles -Niklaus Wirth's programming language work of Pascal [START_REF] Wirth | The programming language Pascal[END_REF] and Modula [START_REF] Wirth | Modula: A language for modular multiprogramming[END_REF], John McCarthy's work on LISP [START_REF] Mccarthy | LISP 1.5 programmer's manual[END_REF], and Jack Dennis's work of programming generality [START_REF] Dennis | Programming generality, parallelism and computer architecture[END_REF].

Conclusion & Future Work

This paper has outlined our proposal of a parallel Turing machine model called PTM. We hope that our work may encourage similar activities in studying parallel Turing machine model. We look forward to seeing significant impact of such studies which will eventually contribute to the success of parallel computing.

We suggest the following topics as future work. A simulator of our proposed PTM should be useful to show how the program execution model and the corresponding abstract architecture work. Two attributes of our PTM may by demonstrated through the simulation -practicability and generality. Since our PTM tries to establish a different model from the previous work, we will show how parallel computation can be effectively and productively represented, programed and efficiently computed under our PTM. Meanwhile, through simulation, we should be able to implement and evaluate extensions and revisions of our PTM. It may also provide a platform to evaluate other alternatives for abstract parallel architecture, such as those that utilize different memory models, or even an implementation that incorporates both shared memory and distributed memory models in the target parallel system.

Fig. 1 .

 1 Fig. 1. (a) Wiederman's model: multiple processing units share a common tape; (b)Generating the new processing units: PU0 copies itself yielding PU1 and PU2, each with its own event in the shared FSM control

Fig. 2 .

 2 Fig. 2. CAM: codelet abstract machine

Fig. 3 .

 3 Fig. 3. A CDG example. (a) Codelet A: inverting the content of memory location a. (b) Codelet B: changing the content of memory location b to 0 (c) A non-conflict CDG

Fig. 4 .Figure 4

 44 Fig. 4. The execution steps of non-conflict example

  The rest of this paper is organized as follows. In Section 2, we describe the existing parallel Turing machine model in detail and suggest possible areas for improvement. Section 3 presents our proposal: a parallel Turing machine model called PTM based on the concept of codelets and codelet graphs. A PTM consists of a codelet graph and a memory. The program of our PTM is represented by a codelet graph (CDG), and the corresponding abstract architecture model is called CAM (codelet abstract architecture). An example is included to illustrate how a parallel program is executed under our PTM. Section 4 briefly reviews related work. Section 5 gives the conclusion of our work and raises some open questions for future study.

	properties, like determinacy, which are keys to the realization of modular
	(parallel) software construction principles by a parallel abstract architecture
	model.
	-We conclude by presenting certain topics as future work on parallel Turing
	machine models.
	2 Existing Work on Parallel Turing Machine -A
	Disappointing Status Report
	2.1 Existing parallel Turing machine proposals
	In 1936, Alan Turing invented an idealized computing device [37], named Turing
	machine (TM). Dr. Turing's model for sequential program execution influenced
	the programming model of sequential computers. Hemmerling [24] first tried to
	propose a parallel computing Turing model in 1979 . His model consists of a
	number of finite state machines working on a shared Turing tape.
	Turing machine
	model studies.
	-A Parallel Turing machine (short named PTM) model is proposed. The
	formulation of the proposed PTM consists of two interrelated parts: a) a
	parallel program execution model; b) an associated abstract architecture
	model serving as a guideline to individual physical machine implementations.
	-We highlight how our PTM addresses some of the weaknesses of the exist-
	ing parallel Turing machine models. The program execution model of our
	PTM is based on the concept of codelets (not threads), that preserve good

Acknowledgements

The authors wish to show their profound gratitude to Prof. Jack B. Dennis at MIT whose pioneer work in computer systems and dataflow have greatly inspired this work. We are grateful to his selfless teaching to his students that served as a source of constant and profound inspiration. We also acknowledge support from University of Delaware and Tsinghua University which provided a wonderful environment for collaboration that led to the successful completion of this paper.