ࡱ> !` `bjbj\\ >>O>  T||||D}$& Ԅ@^Eceee7 %$(h+%%%ccN "|v[0%0&+B<+`+O8TSK%%~p&6L/L  Software Critical Memory: All Memory is Not Created Equal Karthik Pattabiraman University of Illinois at Urbana-Champaign Vinod Grover Microsoft Corporation Benjamin Zorn Microsoft Research September 2006 MSR-TR-2006-128 Microsoft Research Microsoft Corporation One Microsoft Way Redmond, WA 98052 Software Critical Memory: All Memory is Not Created Equal Karthik Pattabiraman University of Illinois at Urbana-Champaign pattabir@uiuc.edu Vinod Grover Microsoft vinodgro@microsoft.com Benjamin Zorn Microsoft Research zorn@microsoft.com ABSTRACT Current hardware memory models treat all data in an address space as functionally equivalent, even though we know that in practice some data is far more important than others. In this paper we introduce Software Critical Memory (SCM), a simple modification to the current flat memory model that recognizes certain data are critical to correct program execution. We introduce the concept of critical memory, created by an operation to map an address range as critical. We add two new memory operations to the current model: verified load and verified store. These are the only operations allowed to consistently read and modify critical memory i.e. no other program store can modify the contents of critical memory with respect to subsequent verified loads. While we focus on software implementations of critical memory, hardware implementations may also be possible. SCM is a general model with a number of important uses. In this paper, we consider using SCM to provide strong atomicity semantics to a software transactional memory implementation that originally supports only weak atomicity. We show that SCM can be implemented with low overhead and the resulting program is more resilient to atomicity violations by errant threads. INTRODUCTION Current hardware and software memory models treat all memory contents as equally important. For example, if an unsafe operation in C or C++ results in a memory corruption (for example, because of a buffer overflow), the results of the entire program are considered undefined, no matter what memory is actually corrupted. Programmers have long known that some program data is more important than other data, and have employed various application-specific, or non-language approaches in such cases. For example, many financial applications use databases to ensure that account information is maintained consistently and durably. In this paper, we describe a new memory model, software critical memory (SCM), which allows programmers to identify and protect data that is critical to the correct execution of their application. The key idea of SCM is that some memory is more critical to the correct execution of an application, and SCM provides mechanisms to identify this memory and protect it from being corrupted by erroneous program stores. SCM adds several new operations to traditional memory models: map_critical and unmap_critical, which designate specific memory addresses as containing critical data, and verified load (vload) and verified store (vstore), which are used to consistently maintain the contents of critical memory. We describe the semantics of these operations in more detail in Section 2. SCM can be used in applications where memory locations can become corrupted, either through unsafe program operations, possible race conditions, hardware transient faults, etc. There has been a great deal of research on solving the problem of adding memory safety to unsafe programs, with solutions ranging from rewriting programs in a type-safe language (e.g., Java) to adding new type annotations to existing C and C++ applications  REF _Ref141839313 \r \h [24], to performing checks at every program load and store to ensure consistency  REF _Ref141839284 \r \h [27]. We believe that SCM offers an attractive alternative to these approaches. Specifically, instead of attempting to prevent all program loads and stores from having bad effects, we limit the scope so that only verified loads and stores have to be consistent. Thus, our approach can be applied incrementally to this problem and also is compatible with large existing bodies of code. One of the important applications of SCM is to improve program reliability. In a companion paper, we describe a runtime system that is built on top of SCM that allows programs to recover from memory errors and hardware transient errors  REF _Ref141867858 \r \h [38]. In this paper, we consider another application of SCM where programmers want assurances that unwanted memory interactions between concurrent threads are not possible. Software transactional memory (STM) is a convenient abstraction that simplifies reasoning about shared data. However, many of the proposed STM implementations provide weak atomicity semantics that is, they do not guarantee the result of an atomic section is consistent if the data being updated in the section is also being modified elsewhere outside an atomic section  REF _Ref141874299 \r \h [3] REF _Ref141873972 \r \h [15]. SCM and STM are orthogonal memory models that can be combined to provide an optimistic concurrency implementation with strong atomicity semantics. In this paper we describe a simple SCM implementation focused on providing strong atomicity semantics to software transactional memory. We have implemented a combination of SCM and STM, and we present preliminary experiments showing that the combination is resilient to errors caused by a non-transactional thread writing to data being modified in the transaction. We present the overhead of STM and SCM in this experiment, and show that for low to moderate error rates, SCM effectively tolerates the errors caused by the errant thread. The remainder of the paper is organized in the following way. In Section  REF _Ref141839077 \r \h 2 we discuss the semantics of software critical memory. Section  REF _Ref141839086 \r \h 0 describes the integration of SCM and STM in our experiments. Section  REF _Ref141839103 \r \h 4 describes our SCM implementation and Section 5 presents our results. In Section  REF _Ref141839119 \r \h 6 we discuss the body of related work and in Section  REF _Ref141839133 \r \h 7 we summarize our work and present possible future directions. DEFINING CRITICAL DATA In this section, we first motivate why critical memory is important. We then define the general concept of software critical memory. Finally, we discuss how SCM can be applied in practice for dealing with arbitrary, unsafe third-party libraries and plugins. Why Some Memory Matters More The core of our argument for critical memory is the observation that in any application, some memory (and the data contained therein) truly matters more than others. The converse of this position, that all memory matters equally, is appealing because it avoids the task of specifically identifying the important data and separating it from the rest. This simplified approach forms the basis of a number of widely deployed technologies intended to improve program correctness. For example, memory-safe languages and runtimes, such as Java or C# provide strong typing, bounds checking, and automatic garbage collection  REF _Ref141846463 \r \h [13] REF _Ref141846561 \r \h [35]. While there are clear software engineering benefits from using these languages, they currently fail to completely address important and practical reliability problems. For example, both Java and C# allow unsafe code to execute through explicit mechanisms or via a foreign function interface that allows libraries written in C and C++. A similar challenge faces techniques that attempt to ensure that programs written in C and C++ are entirely memory safe  REF _Ref141839313 \r \h [24] REF _Ref141839284 \r \h [27] REF _Ref141839724 \r \h [20]. Practical constraints on such approaches include the issue of linking with third-party libraries, where source code is not available and calling conventions and data representations must be maintained for compatibility. In practical terms, programmers have to anticipate potential errors in the execution of their applications and handle them as best they can. At one end of the spectrum, data that is extremely critical is relegated to the heavyweight mechanism of an external database, incurring the task of determining what should be in the database, how it should be organized, and what overhead using the database will incur on the program execution. At the other end, exceptions provide a means of identifying exceptional conditions during execution and handling them. Ad hoc techniques to ensure that some of the data is in a consistent state when an exception is raised allow programs to recover from such events. For example, if an exception is raised in a word processing application, the handler code may need to ensure that the document being processed is consistent in memory before allowing it to be written out to disk. Chandra et al.  REF _Ref141851789 \r \h  \* MERGEFORMAT [9] showed that applications with built-in state-saving and error recovery mechanisms can recover from a broad range of software faults more often than applications that use generic techniques such as system-level checkpointing. This recovery mechanism is typically written by the programmer who makes certain assumptions about the consistency of the state saved by the application for the recovery. The notion of critical data formalizes these assumptions and allows the recovery mechanisms to recover the application with well-defined semantics. Ultimately, many applications tolerate memory inconsistencies well, and are robust in general use. Our practical goal is to give programmers, who are already dealing with possible inconsistencies, mechanisms that allow them to be even more effective. Software Critical Memory Semantics SCM allows a memory address used in the program to be marked critical using the map_critical operation. This places the data in the memory address under the protection of SCM, and guarantees that the data is safe from unintended modification, provided that it is accessed according to the following rule: all loads and stores to the memory address in the program must be performed by means of special operations called verified loads and verified stores. A verified load or store is defined as a static instruction that could potentially read from or write to critical data and is allowed by the semantics of the program to do so (by programmer intent). SCM guarantees that any update made to critical data through a verified store will correctly update the critical data, and any update made to the critical data through a normal store will not be able to update the critical data (in a consistent way). Similarly, any read of the critical data done through a verified load will see a consistent version of the data, whereas any read of the critical data done through a non-critical load may or may not see a consistent version. By consistent, we mean that a verified load to a critical location will read the value written by the last verified store to the critical location in the program. SCM ensures that any intervening updates to the critical data by non-verified stores will be transparent to the verified-load. A verified load or store conveys the programmer intent to read from or write to critical data and is allowed by the semantics of a valid C or C++ program to do so. Thus, while the majority of an application may not be type-safe, we assume that the subset of the program that does verified loads and stores is correct and well-checked (ideally statically, for example using types). Any code that violates memory safety should not be allowed to perform verified stores and hence would not be able to overwrite the critical data. Thus, a central idea of SCM is that it allows programmers to preserve the consistency of critical data even in the presence of arbitrary unsafe code. Note that the guarantees provided by SCM extend only to the critical data, and SCM does not provide any guarantees on the non-critical data. SCM also does not provide protection against (1) computation errors that incorrectly update critical data through a verified load or store. We assume that the programmer has used some other mechanism (e.g. executable assertions) to ensure that critical data is updated correctly by a verified store. (2) SCM does not protect critical data from errors that change the control-flow of the original program and cause it to either incorrectly update critical data through a verified store or fail to perform a correct verified-store to critical data. We assume that important control-flow information is also part of the critical data, or that other mechanisms to check the control flow are present in the program similar to those in  REF _Ref141871592 \r \h [1]. In a program, the same static instruction may access both critical data and non-critical data depending on the program context and execution flow. Hence, it is necessary to mark any load or store that may-alias critical data as a verified-load or verified-store. When non-critical data is accessed by a verified-load or verified-store, the effect of the operation is similar to an unverified load or store on the non-critical data. However, a store that would never access critical data (must not alias) should be marked as an unverified store, so that it does not accidentally overwrite critical data as a result of a memory error. Similarly, an unverified load is allowed to read from critical data, but no guarantees on the consistency of the data read are provided by SCM. The semantics of SCM with respect to verified and unverified loads and stores on critical and non-critical data are summarized in  REF _Ref139344027 \h Table 1. Table  SEQ Table \* ARABIC 1: Interactions between SCM loads and stores Type of OperationData being AccessedGuarantees provided by SCMVerified-LoadCritical DataGuarantees that the value read is the one written to by the last verified-store to this location.Verified-StoreCritical DataGuarantees that the update is reflected in the critical data and is visible to future verified loads on the critical data.Verified-LoadNon-Critical DataThis is equivalent to an unverified-load on the non-critical data. Verified-StoreNon-Critical DataThis is equivalent to an unverified-store on the non-critical dataUnverified-LoadCritical DataThe value read by the load depends on the compatibility model (defined in Section  REF _Ref141872536 \r \h 2.3) Unverified-StoreCritical DataThe effect of the update is not reflected in the critical data and future verified loads will not see this update.Unverified-StoreNon-Critical DataThis updates the non-critical data similar to a regular store in a program. Unverified-LoadNon-Critical DataThis reads from the non-critical data similar to a regular load in a program. Table  SEQ Table \* ARABIC 2: Summary of SCM operations Name of OperationArgumentsSemanticsmap_criticalAddressMarks the address as critical and clears its contents.unmap_criticalAddress Marks the address as non-critical, and preserves its contents.verified_loadAddress, RegisterDoes a verified load of the address into the registerverified_storeAddress, RegisterDoes a verified store of the register contents to the addresspromoteAddressMarks an address as critical and preserves its contents. SCM also provides an unmap_critical operation to designate when a memory address becomes non-critical. Once a critical address has been unmapped, it can be accessed using normal loads and stores and verified loads and stores to that address have the same effect as regular loads and stores. Addresses may be unmapped, for example, when the programmer is done using the memory region and de-allocates it (using a free operation). This can also happen when calls to third party code are made by the program, as explained below. A final operation, promote, both maps an address as critical, and promotes the contents of that address to be critical. The primitive operations of SCM are summarized in  REF _Ref139344059 \h Table 2. Reference Interleaving One of the uses of SCM is to allow applications to protect their critical data despite potential unsafe operations performed in third-party library code. Note that it may be necessary to allow library code to update part of the programs critical data. For SCM to be most widely adopted, it must be possible to use SCM in an application that calls a library that has no knowledge of SCM. In considering the semantics of the interleaving of SCM verified loads and stores with other program loads and stores, there is a spectrum of choices about the semantics that on one hand constrain the SCM implementation, but on the other hand provide greater degrees of compatibility with non-SCM aware libraries. We consider three possible degrees of compatibility and illustrate them in  REF _Ref141872870 \h Figure 1. Instruction SequenceWeak Compat.Strong Compat.Extreme Compat.map_critical x vstore 5 -> x load x store 6 -> x load x vload x load x x = 5 x = undef x = 5 x = 5 x = 5 x = 6 x = 5 x = 5 x = 5 x = 6 x = 5 x = 6Figure  SEQ Figure \* ARABIC 1: Compatibility Interleaving Semantics The first column illustrates a sequence of interleaved memory operations, and the remaining three columns show the value of the variable x assuming different approaches to compatibility. First note that the verified store of 5 to x is seen in all cases by the subsequent verified load. The difference between these approaches lies in the effect of unverified stores and subsequent loads to the critical location. Weak compatibility makes no guarantees about the effects of unverified stores to critical memory locations. As a result, in the figure, the unverified store of the value 6 to a critical location does not necessarily imply that the subsequent unverified load will see that value. The result of that load is thus undefined. This semantics gives the underlying SCM implementation the option to normalize the contents of critical memory at any time (meaning, make the memory location consistent with respect to verified loads). Of course, these semantics imply the third party libraries would routinely break if they ever accessed critical memory locations in an application. Strong compatibility requires that subsequent unverified loads to addresses will see the value stored by unverified stores, assuming that an intervening verified load or store hasnt occurred. Thus, in the example, the subsequent load of x will consistently see the value 6. Subsequent verified loads to the location still return the value stored by the verified store (5), with loads after that also returning 5. With this approach, third party libraries will be able to modify critical data as if it were normal memory, but the effects of these updates will not be visible to subsequent verified loads in the application. We expect strong compatibility is the most practical balance of implementation flexibility and compatibility. Extreme compatibility takes the stronger position that loads and stores to critical addresses are completely independent of verified loads and stores to the same addresses. Thus, in the example, the final unverified load of x sees the value of the last unverified store, and not the value of the last verified load. This model may be required to ensure the correctness of the library function if it performs call-backs into the application code containing verified-loads and verified-stores. Libraries In this section, we consider what is required when an application is calling potentially unsafe library code that is not SCM-aware (that is, does not allocate critical data or perform verified loads and stores). In the case where the library code does not need to modify critical data, the code can execute as written and the loads and stores it does to non-critical data occur as if SCM was not being used. If the library performs unverified loads of critical data, as long as it has not performed unverified stores to those addresses, the values read will be consistent with the values written to the addresses by the main application prior to calling the library. If the library is required to modify critical data, then additional actions are necessary. We illustrate the process by example, which is similar in structure to a copy-in, copy-out semantics. Consider  REF _Ref141872887 \h Figure 2, where the value at address x needs to be modified by a library routine. map_critical x vstore 5 -> x unmap_critical x call library_foo promote xFigure  SEQ Figure \* ARABIC 2: Calling sequence to 3rd party library In the example, the address x is first unmapped before calling the library, allowing the unverified stores in the library to update the address in a way that will be visible to the main program. After the call, the address x is promoted, simultaneously making the address critical again, and making the current value of the address the critical value. While we have assumed non-SCM-aware libraries, in practice, the libraries may also be written to use their own critical memory. This leads to the issue of interfering critical memory updates between the libraries and the application. One approach to supporting composition of libraries and applications that use critical memory would be to associate a unique key with each compilation unit (e.g., library or application) and tie each static critical memory operation in a unit to the units unique key. In this case, critical memory that is mapped with one key could only be updated with a verified store that had the same key associated with it. The main difference between SCMs approach to supporting third-party libraries and an approach such as Software Fault Isolation (SFI)  REF _Ref140403887 \r \h [36] is that SFI aborts the program upon encountering a store outside the protection domain or turns the store into a null operation. Both these actions would result in the program crashing or the library function executing incorrectly (as its state would be inconsistent with respect to its loads and stores). A primary goal of SCM is to allow the incorrect library functions that have memory errors to continue execution and see a consistent view of memory (with strong or extreme compatibility semantics). At the same time, SCM guarantees that the critical data of the application is not impacted by the memory errors present in the library function, as long as the library does not perform verified stores to the applications data. Applications of SCM A primary use of SCM is to increase program robustness by giving programmers a mechanism to identify and protect critical application data from unsafe operations in code outside their control. We have already discussed how SCM can be used to limit the effects of unsafe library code on an applications critical data. In an accompanying paper  REF _Ref142213393 \r \h [38] we describe an SCM implementation intended for this purpose, and present results of its effectiveness. In this paper, we consider the related problem of providing strong atomicity semantics for software transactional memory. Providing Local Immutability One SCM application attacks a problem related to data immutability. A typical exploit of non-immutable data involves a resource that requires some check. For example, a program that is about to open a file for update might check to see if the file is in a particular scratch directory to limit the effect the update can have on the rest of the file system. The exploit involves a race condition whereby the string that was checked is updated by another thread between the time of the check, and the time the file is actually opened. If the string were truly immutable, then the subsequent update would be impossible, and the problem is solved. Language memory models, such as Javas, add complexity to guarantee such immutability  REF _Ref142214247 \r \h [7] REF _Ref142214307 \r \h [25]. Providing truly immutable data is strictly a stronger guarantee than is necessary to fix this problem. All this is required is to guarantee that the memory locations in which the string is stored cannot be modified by other threads between the time the check is done and the time the action is taken. We can use SCM to accomplish this effect by doing a map_critical of the memory locations before the check, using a verified load when the operation is performed, and doing an unmap_critical after the operation. Non-verified updates to these locations in the time between the check and the operation are ignored by the verified load. In this way, SCM can provide the illusion of local immutability, which is one element of the broader guarantees provided by the general mechanism of software transactional memory. While solving the immutability problem with SCM is possible independently of using it with SCM, SCM and STM can also be considered together, as we discuss in the next section. Potential Optimizations While performance is not the primary goal of SCM, there are performance opportunities implied by introducing SCM into a program that we describe here. The first opportunity is based on the observation that verified loads and stores form a small subset of all loads and stores in an application. If we assume weak compatibility semantics, verified loads and stores can be repositioned independently relative to other loads and stores in an application. For example, in the code sequence: Vstore 5 -> x Loop: (no verified operations) Store 100 -> y ; may alias with x Store 1000 -> z ; may alias with x Vload x Goto LoopThe verified load of x can be moved out of the loop because the intervening loads and stores are guaranteed not to change the value of x. One can think of the verified loads and stores as forming a well-typed independent subset of the computation being performed by the rest of the program. As a result, the optimizer can more aggressively reorder operations because it knows that they are independent. A second optimization benefit of SCM is the ability to reason locally about critical values. If addresses are mapped as critical and local to a component (using the key-based technique mentioned above), then the optimizer has the guarantee that other components, even executing in the same address space, cannot modify the critical addresses unless they are specifically allowed to. Thus, critical memory provides data-centric guarantees of isolation even within the same address space. One way to think of SCM is that it is embedding a smaller, simpler, well-typed program (which operates only on critical data) within another program. This simpler program provides more opportunities to the optimizer than the original program, which in C and C++ often has aliases that confound attempts at static analysis. Strong Atomicity with SCM Transactional memory provides transaction semantics to individual memory operations  REF _Ref141874355 \r \h [17] REF _Ref141846747 \r \h [1]. Such transactions are currently being intensively investigated because they offer potential benefits in simplifying concurrent programming  REF _Ref141846869 \r \h [15]. Software transactional memory offers the benefits of transactional memory without hardware support. Several recent publications have demonstrated that STM can be implemented with relatively low overhead  REF _Ref141874299 \r \h [3] REF _Ref141846898 \r \h [15] REF _Ref141773608 \r \h [1]. These implementations use optimistic concurrency control for transactional reads and write-in-place semantics for transactional writes to achieve high performance. Unfortunately, to achieve this performance, these STM implementations provide weak atomicity they assume all writes to transactional memory occur strictly inside transactions. If other threads write to these locations outside of transaction boundaries, the outcome of the program is undefined. Recent work has suggested low-overhead approaches to providing strong atomicity semantics to STM implementations using lock-based source-to-source transformations of Java programs  REF _Ref141842750 \r \h [18]. We suggest another alternative here using SCM to temporarily hide the effects of updates to memory from other threads during the execution of an atomic section. The high level view is that for each memory location modified in an atomic section, the software transactional memory system provides support for conflict detection and undo, while the software critical memory system independently provides resilience to external modification outside the thread. For the most part, SCM verified load and store operations are paired with complementary STM operations. In  REF _Ref141777394 \h Figure 3a, we show a simple example of a transactional code that atomically accumulates a local value (localSum) into a shared variable (Total->Sum).  REF _Ref141777394 \h Figure 3b shows the pseudo code that corresponds to this fragment, with STM primitives inserted using the approach described in  REF _Ref141846898 \r \h [15]. In this translation, we use C++ exception handling to encapsulate the transformed body of the atomic block. A runtime primitive TxStart creates a new transaction container. The accesses to the shared variables are done via runtime primitives: TxRead and TxWrite. TxCommit primitive is called at the end of the atomic block to complete the transaction. If the transaction state is valid and there is no conflict with another transaction the effects of the transaction are published to shared memory, otherwise an internal exception (TxError) is raised. The handler for this exception rolls back the transaction state and re-executes the transaction body. The main problem with the code in  REF _Ref141777394 \h Figure 3b is that a third thread that does not follow the transaction protocol can write to the shared variable Total outside the atomic section and corrupt it. The goal of using SCM is to prevent this from happening by restoring the contents of the Total variable to its contents within the atomic section. As a result, calls to verfied_store and verified_load operations must be inserted within the atomic section along with the TxRead and TxWrite operations. These will ensure that the value of the Total variable cannot be updated outside the atomic section. Original STM program // Total is a struct containing a global integer, and is shared while (element = iter->get() ) { localSum = element->value(); atomic { Total->Sum += localSum; } }STM program with primitives exposed while ( element = iter->get() ) { localSum = element->value(); void * Tx = TxStart(); RestartLabel: try { TxRead(&Total->Sum); tmp = Total->Sum; tmp = tmp + localSum; TxWrite(&Total->Sum); TxCommit(); } catch (TxError * errorCode) { TxRollback(errorCode, Tx); goto RestartLabel; } }STM/SCM program with primitives exposed while ( element = iter->get() ) { localSum = element->value(); void * Tx = TxStart(); RestartLabel: try { verified_load(&Total->Sum); TxRead(&Total->Sum); tmp = Total->Sum; tmp = tmp + localSum; TxWrite(&Total->Sum); verified_store(&Total->Sum, tmp); TxCommit(); } catch (TxError * errorCode) { TxRollback(errorCode, Tx); goto RestartLabel; } }Figure  SEQ Figure \* ARABIC 3: Example code showing STM, Low-level primitives and SCM/STM integration The code instrumented with the SCM calls is shown in  REF _Ref141777394 \h Figure 3c. In our implementation, the verified_load call does not actually perform the load, but merely checks if the data value loaded is consistent. The verified_load is inserted just before the TxRead so that the value recorded by the STM library functions is consistent with the values observed by the SCM implementation. Similarly, the verified_store is inserted after the actual store, so that the value is only updated if the transaction is not rolled back. In addition to the instrumentation added, two other mechanisms are needed for integrating SCM and STM. These are as follows: When a transaction is rolled back, STM restores the value of the variables modified within the transaction to their original values. This restoration must be made visible to SCM, as otherwise it would restore the values to their modified values assuming that the update had been made in error. Hence, a call-back mechanism is provided within STM to call a user-defined function when a transaction is rolled-back and just before it is re-executed. This user-defined function must perform the promote operation on all critical data that the STM restores to their original values (In the example, this is the value of Total->Sum). When a transaction is committed, STM stores the values written within the transaction to permanent state and updates the contents of memory locations with these values. Although in the example provided, the transaction is committed immediately after the last verified_store, in larger programs, there may be other intervening instructions between the last update to the shared state and the transaction commit. In such cases, it must be ensured that the value written to the permanent state is correct and is indeed the value written by the last verified_store. This is done by calling a user-defined call-back function from within STM just before transaction commit, which performs a verified_load operation on every value that is written to the permanent state (In the example, this is Total->Sum) Both these call-back functions must be provided by the application program and registered with the STM libraries prior to using atomic sections in the code. Implementation In this section, we describe briefly one possible implementation of SCM for objects allocated on the heap. This implementation is called Samurai and uses replication to achieve the semantics of SCM with high probability. This section discusses a simplified version of Samurai for ensuring strong atomicity in STM. We assume that the code is free of memory errors, that is, no thread writes outside its allocated memory buffers (within or outside a transaction). Note that the complete implementation of Samurai does not make this assumption and can be used to recover programs with memory errors. A description of the complete Samurai implementation can be found in  REF _Ref141867858 \r \h [38]. Implementing Map/Unmap Critical Samurai implements the SCM semantics only for dynamically allocated heap data. Hence, all data that is required to be protected by SCM must be allocated on the heap. This is traditionally done with the malloc() and free() functions in C. Samurai provides its own versions of malloc() and free() called critical_malloc() and critical_free() to allocate and deallocate critical data. The Samurai heap is organized as BIBOP (Big-Bag of Pages) style partitions, as with the Diehard  REF _Ref140320328 \r \h [4] and PHKmalloc  REF _Ref141841481 \r \h [21] systems. Essentially, this means that memory can be allocated from the heap only in certain sizes (usually distinct powers of two) and objects of the same size are in the same partition. A partition is a chunk of memory with a fixed starting address. At application initialization time, Samurai divides the heap into partitions of fixed sizes (one for each power-of-two object size) and stores the starting addresses of the partitions. When an object of a certain size is requested from the heap, the object size is rounded to the next higher power of two and the partition for that object size is searched to find a free chunk to accommodate the object. Since the partition contains only objects of a fixed size, the search is essentially a linear probe into the partition. When an object is allocated using the critical_malloc function, Samurai allocates an additional object that mirrors the contents of the original object. This object is allocated transparently to the application, and is called the shadow of the original object. A pointer to the shadow is stored as part of the heap metadata of the original object, at its beginning. When an object is freed using the critical_free function, the pointer is followed and the shadow is freed as well. Implementing Verified Loads and Stores Samurai implements verified loads and verified stores by providing function calls with the same syntax as the equivalent SCM operations. A verified store to a critical object (an object allocated with critical_malloc) updates both the original object as well as its shadow, with the contents being stored. A verified load to a critical object checks the consistency of the location being loaded by comparing it with the corresponding location in the objects copy and if a mismatch is found, the orepairs the object by copying the contents of the shadow back to the original. The contents of the objects shadow are always correct, since as per our original assumption, the code is free of memory errors and since the shadow is maintained transparently to the application, the application cannot overwrite the shadow without incurring a memory error. Since the verified load repairs the contents of the original object, subsequent loads (both verified and unverified) will see the repaired contents. Hence, Samurai implements the SCM semantics with the strong-compatibility model. Both the verified load and verified store operations require the ability to locate the shadow of an object given a pointer within the object. Since a pointer to the shadow is stored at the beginning of an object (as part of the metadata for that object), a mechanism is needed to locate the start of an object given a pointer to an internal location in the object. This can be done efficiently due to the BIBOP-style organization of the Samurai heap and is best illustrated with an example as follows: Consider a pointer addr=0x8023f48 that points within some object on the heap. Assume that the memory region start=0x8000000 to end=0x9000000, is used by Samurai for allocating objects of size 128 bytes. Hence, the size of the object can be inferred to be 128 bytes. Compute the offset within the partition, offset = addr start = 0x8023f48 0x8000000 = 0x23f48 The index of the object within the partition can be computed as, index = offset / size = 0x23f48 / 0x80 = 0x47E. Therefore, the base address of the object is base = start + (index * size) = 0x8000000 + 0x47E * 0x80 = 0x8023F00. This is the base-address of the object which is pointed to by the pointer 0x8023f48. Note that the above operation takes constant time. Also, since Samurai rounds of object sizes to powers of two, the multiplication and division operations on the size can be performed using bit-shift operations, making them very fast in practice. Discussion The strong-atomicity guarantees provided by SCM (and hence Samurai) are probabilistic in nature. In other words, the semantics of SCM are implemented with high probability by Samurai, but not with 100% probability. This is because (1) SCM and STM are implemented separately and are not integrated in one implementation and (2) The interface provided by SCM inherently has a window of vulnerability due to the ordering of SCM operations with respect to loads and stores in the atomic section and (3) The implementation of SCM is not 100% error-proof and has some windows of vulnerability. In the first case, there exists a window of vulnerability between a verified load operation and the TxRead operation, during which an unsafe thread (outside the transaction) could corrupt the value being loaded, and hence SCM and STM would see different values. There is also a window of vulnerability between the TxWrite operation and the verified store operation, during which an unsafe thread could corrupt the shared variable, although this is less likely to be an issue since the verified store uses a local variable to update the contents of the shared variable. These issues could be avoided or minimized by an implementation that tightly couples the SCM and STM operations, and is not an inherent limitation of SCM. In the second case, there exists a vulnerability window between when an SCM operation is performed and when the actual load or store is done. Since the verified load operation is performed before the actual load operation, an unsafe thread could corrupt the value of the shared variable between the verified load and the actual load. This would result in the load operation reading the wrong value of the shared variable, and may result in incorrect computation of the result. This is likely to be a problem for any software implementation of SCM, as there will exist a window (however small) between checking the consistency of the data and loading it into a register, during which the value could get corrupted by another thread. One way to solve this problem is to exploit hardware support for a verified load operation that performs both the consistency checking as well as the resulting load (an atomic check and load operation). The third source of vulnerability is because the implementation of Samurai is itself not immune to corruptions from an unsafe thread. A verified store operation in Samurai first updates the original object and then subsequently copies the contents to the shadow copy. It is possible for the value to be corrupted in the midst of this copy by an incorrect thread, resulting in the copy being updated incorrectly. METHODS AND RESULTS Measurement Methodology The goal of our experiments is to demonstrate the integration of SCM and STM on a small benchmark program and to study its effectiveness at protecting critical data. The benchmark program chosen is an array reduce program that computes the sum of elements in an array using atomic sections. The program consists of about 400 lines of C code and has two atomic sections each comprising of less than 10 lines of C code. The program uses an atomic iterator to extract elements from an array and add them to a shared variable Sum within an atomic section. The Sum variable is protected with SCM by allocating it on the heap using the critical_malloc function. An automated compiler pass built on top of the Phoenix infrastructure  REF _Ref141842408 \r \h [23] is used to insert the SCM and STM primitives inside the atomic sections of the program. The STM implementation is based on  REF _Ref141873972 \r \h [15] and was developed at Microsoft. All experiments are conducted on a dual-P4 Xeon processor (3.4 Ghz) with 2GB of RAM on a machine running Microsoft Windows XP SP2. Although the processor supported hyper-threading, this was disabled by default on our machine. All times were measured using the Windows timeGetTime() API call. Unless otherwise stated, this program was executed with two threads. During the execution of the program, each thread enters and leaves the atomic section a total of 100000 times. Since this program was developed as a benchmark for STM, it spends a significant amount of time in the atomic section Effectiveness In order to measure the effectiveness of the approach, a fault-injection experiment is performed in which a third thread is spawned by the application, which performs unsafe operations on the shared variable Sum without following the transaction protocol. In other words, it modifies Sum outside of an atomic section, and hence is unsafe with respect to the transaction protocol. We call this thread the faulty-thread. We ensure that the faulty thread can perform at most one unsafe modification to the variable Sum inside a critical section. We can also control how frequently the faulty thread performs the unsafe modification, by varying the fault-period. A fault-period of N means that the unsafe modification is performed every N times the atomic section is entered by any of the correct threads. The effect of the faulty-thread is to set the value of the Sum variable to zero, which would result in the overall value of Sum being computed incorrectly. The final computed value of Sum is compared offline with the correct value to determine if the faulty thread was successful in corrupting the value of sum.  Figure  SEQ Figure \* ARABIC 4: Results of Fault-injections into SCM/STM The results of the fault-injection experiment are shown in  REF _Ref141779679 \h Figure 4. The fault-period was varied between 10 and 200 in increments of 10. For each value of the fault-period, 100 trials were performed and the percentage of erroneous trails was plotted. As can be seen from  REF _Ref141779679 \h Figure 4, for all values of the fault-period, the number of error manifestations with STM alone is more than the number of error manifestations when SCM and STM are combined (For STM alone, the error manifestation is nearly 100% across the range of fault-periods considered). Further, the number of error manifestations with SCM decreases as the fault-period is increased, as probabilistically the faulty-thread has a greater chance of corrupting the shared variable at higher fault-rates (lower values of the fault-period). For example, with a fault-period of 10, about 90% of the runs are erroneous, whereas with a fault-period of 200, less than 10% of the runs are erroneous. The reason that the error-manifestation is not 0% (with SCM) is due to the probabilistic nature of the protection provided by the SCM implementation, as explained in Section 4.3. Performance Overhead We also measure the execution time of the application when SCM and STM are deployed together. In these experiments, the number of threads is varied from 1 to 16 in powers of two, and there is no faulty-thread.  REF _Ref141773619 \h Figure 5 shows the execution time (in milliseconds) of the application with STM and with SCM/STM combined as a function of the number of threads in the application. The top line in the graph represents the overhead of SCM combined with STM, while the bottom line represents the overhead of STM alone. The difference between the two lines represents the overhead of SCM. As can be observed from  REF _Ref141773619 \h Figure 5, this difference varies between 1% and 5% of the execution time.  Figure  SEQ Figure \* ARABIC 5: Scaling of SCM and STM with number of threads It can be observed from  REF _Ref141773619 \h Figure 5 that the execution time decreases drastically as the number of threads is increased from 1 to 2. There is a marginal decrease when it is increased from 2 to 4 and a slight increase in execution time when it is increased beyond 4. This is not because of the lack of scalability of STM but because we are running the experiment on a dual-processor machine. The available hardware parallelism is at most two and hence, there is no real benefit from increasing the number of threads beyond 2 (in fact there may even be a negative effect as the probability of collisions within a transaction is higher, thereby resulting in more transactions being rolled back). An interesting point to note is that the overhead of SCM with respect to STM remains about the same as the number of threads is increased from 1 to 16. This suggests that combining STM with SCM does not constitute a scalability bottleneck. We also tested the resilience of the application with both SCM and STM as the number of threads is increased beyond 2 (all the way through 16) and found that the application protected with SCM is more resilient to faults than the one with STM alone. The results for the fault-injection experiment are not reported here due to space constraints. RELATED WORK Address Space Protection Address space protection has been a topic of extensive research for many years. Address translation and paging hardware allow efficient page-level protection mechanisms  REF _Ref141864876 \r \h [34], while virtual memory provides address space isolation between processes  REF _Ref141848067 \r \h [11]. Mondriaan Memory Protection (MMP), is based on hardware that allows fine-grained protection domains, although it has never been implemented  REF _Ref141848089 \r \h [37]. These approaches attempt to detect and prevent inappropriate accesses between system entities, and typically raise an error or exception when illegal operations are performed. SCM differs from these mechanisms in two important ways. First, like MMP, SCM is fine-grained and requires programmers to explicitly identify the critical data in their application. Second, instead of raising an error when an illegal store is performed, SCM allows the store to continue while still preserving the consistency of the critical data. Many papers have explored approaches to integrating untrusted code into a trusted code base. Examples include OS kernel extensions (Vino  REF _Ref141848155 \r \h [30], SPIN  REF _Ref141848157 \r \h [5] and Nooks  REF _Ref141848159 \r \h [33]), application plug-ins (SFI  REF _Ref140403887 \r \h [36]]), server hosted applications (web CGI), etc. SCM differs from this work in our emphasis on protecting critical data instead of isolating untrusted code. We do not intend SCM as a mechanism to provide general security guarantees, and as a result, SCM will not protect the integrity of non-critical data in the presence of untrusted code. Transactional Memory Software Transactional Memory (STM) is an active area of research. Harris et al.  REF _Ref141873972 \r \h [15] and Adl-Tabatabi et al.  REF _Ref141874299 \r \h [3] describe two very similar approaches which are the basis of our work. In this approach they describe the implementation of atomic blocks which use exception handling to represent the abort and rollback semantics of transactions and decomposed operations like Start, Commit, Rollback, OpenForRead and OpenForWrite. A failing transaction throws a special exception which triggers the re-execution of the transaction. These approaches also prescribe in place updates and require STM primitives that create the read, write and undo logs. Weak atomicity is considered by some researchers to be a critical problem for current STM implementations  REF _Ref141842729 \r \h [7]. An analysis of weak atomicity is described by Blundell et al.  REF _Ref141842533 \r \h [6]. Lev et al. describe an approach for dealing with problems of weak atomicity  REF _Ref141842549 \r \h [22]. Their approach implicitly tracks object visibility at runtime and identifies exactly which objects need to be guarded by transactions. They also describe optimizations to reduce the runtime overhead of their approach. While their approach attempts to correctly wrap all share-object operations in transactions, our SCM-based solution allows non-transactional updates, but prevents the updates from having an effect. Hindman and Grossman describe a lock-based approach to providing strong atomicity in Java without assuming hardware support or transactional memory  REF _Ref141842750 \r \h [18]. Using protocols for automatically acquiring locks, they are able to provide strong-atomicity and guarantee no deadlocks. While their approach has overhead, they show how to reduce the overhead with analysis-based optimizations. However, their approach works only for Java (which is type-safe) and it is unclear how to generalize this for C and C++ programs. Recently, researchers have proposed combining exception handling with transaction mechanisms, allowing rollback of state changes if an exception is raised  REF _Ref141849676 \r \h [31]. Memory Safety There has been considerable work on bringing the type-safety properties of languages such as Java to C and C++. Cyclone is one such system that allows programmers direct control over memory and uses region-based allocation and explicit safe de-allocation to achieve memory safety  REF _Ref141840914 \r \h [14]. It augments C with an advanced type system and typically requires programmer intervention to manage memory accordingly. CCured uses static analysis and type-inference to classify pointers in the program based on their usage  REF _Ref141839313 \r \h [24]. It finds that most pointers in the applications considered were type-safe and hence need not be checked at runtime, while a small fraction of the pointers were wild and could write to any arbitrary memory location. These pointers need to be bounds-checked at runtime, and this checking needs to be done for every pointer in the program that could not be proved to be type-safe statically. Omitting to check even a single pointer breaks the memory safety guarantees of the system. Also, C-Cured requires engineering effort to make it compatible with library code, as it modifies the format of pointers in the program  REF _Ref140318656 \r \h [10]. A third approach to ensure memory safety of C programs is Software-Fault Isolation (SFI)  REF _Ref140403887 \r \h [36]. In SFI, each module in a program is given the illusion of executing in its own address space and the compiler/binary-rewriting tool ensures that one module cannot access memory outside its pseudo-address space. This can be implemented in hardware using protection domains, but comes at a performance cost. More importantly, it requires modifications to the machine code of the application and cannot support arbitrary third-party libraries, whose binary is unavailable at link time (such as dynamically loaded libraries). Singularity is an operating system that was designed from the ground-up to provide reliability guarantees to applications. The Singularity approach  REF _Ref140404365 \r \h [19] is to write everything in type-safe languages and prove memory safety at compile-time. It allows contracts to be specified for third-party code and enforced statically. However, it requires considerable effort from the programmer to rewrite application code to be type-safe. It also requires third-party code to be type-safe, which may not be possible in practice. A recent approach to protect the control-flow of a program for security was proposed by  REF _Ref141871592 \r \h [1]. The goal of this approach is to ensure that the programs control flow is not subverted at runtime by an attacker or error. In a companion paper, they show how control-flow integrity combined with memory-safety for the control-data can provide provable security guarantees to the application  REF _Ref141871628 \r \h [2]. A system such as SCM could be used to achieve memory-safety guarantees for the control data. Error-Tolerance Diehard  REF _Ref140320328 \r \h [4] is a system to tolerate memory errors in an application. The goal of Diehard is to provide probabilistic soundness guarantees for applications that allow them to continue execution even in the presence of memory errors. However, Diehard protects all data equally and does not distinguish between critical and non-critical data. Diehard offers two modes of protection: replicated and unreplicated mode. Most of the protection guarantees provided by Diehard apply only to the replicated mode, in which the entire process is replicated. SCM provides similar guarantees as the replicated mode of Diehard for a subset of the applications data, without requiring process-level replication. Recently, there has been work on failure-oblivious computing  REF _Ref141871663 \r \h [28] where the idea is to continue execution after a memory error, by ignoring illegal writes and manufacturing values for illegal reads. The problem with this approach is that after a memory error has occurred and the application crashes, the state of the application is undefined and the application may perform harmful or malicious actions upon continuation. The Rx system  REF _Ref140320309 \r \h [25] combines checkpointing with logging to recover from detectable errors such as crashes. Upon a failure, Rx rolls back to the latest checkpoint and re-executes the program in a modified environment, depending on the memory error encountered. Rx is unsound in that it cannot detect latent errors that do not lead to program crashes but result in incorrect outputs. Also, not all applications can be rolled back upon a failure. DyBoc  REF _Ref140404623 \r \h [32] uses execution transactions to recover from buffer overflow attacks. The idea is to treat function calls as transactions that can be aborted when a buffer overflow is detected. This also has the problem that not all applications can be rolled back, and that the rollback is restricted to the current function when in fact, the error could have occurred anywhere in the program. Many internet systems have been written with error-tolerance in mind. For example, search engines provide lower-quality search results when an error occurs rather than taking the entire system down  REF _Ref141851815 \r \h  \* MERGEFORMAT [12]. They also replicate data that is critical to the application at multiple sites, so that the application can continue even when some of the sites become unavailable. SUMMARY AND FUTURE WORK We have described software critical memory, a new memory abstraction that allows programmers to separate critical data from non-critical data and provides guarantees about the consistency of critical data in the presence of code that may unintentionally modify it. Critical memory provides two important benefits. First, unintended writes to critical data do not affect the data, preventing consistency errors. Second, libraries and components unaware of critical memory require no changes in cases where they do not modify critical memory and will continue to execute even when they do modify it incorrectly. Critical memory is a mechanism that can be used to provide increased robustness to applications with memory safety errors. In this paper we explore the use of software critical memory to increase the robustness of software transactional memory in the face of strong atomicity violations. In preliminary experiments, we show that the overhead of adding SCM to STM is low (1-5%) and that the presence of SCM provides probabilistic strong atomicity semantics to our STM implementation. In the future, we intend to extend our experiments to consider more complex STM applications. Our current implementations of SCM and STM are loosely coupled, and we plan to investigate the robustness and performance benefits possible by more tightly integrating them. More generally, we will consider the implications of identifying critical data in a program and attempt to understand properties of the program subset implied by a particular choice of critical data Acknowledgements We greatly appreciate the feedback received by reviewers of this work, including Emery Berger and Pramod Joisha. We thank Emery Berger for making the Diehard software publicly available. REFERENCES Martn Abadi, Mihai Budiu, lfar Erlingsson, and Jay Ligatti, Control-Flow Integrity: Principles, Implementations, and Applications. To appear in Proceedings of the 12th ACM Conference on Computer and Communications Security (CCS'05), Alexandria, VA, November 2. Martn Abadi, Mihai Budiu, lfar Erlingsson, and Jay Ligatti. A theory of secure control flow. To appear in Proceedings of the 7th International Conference on Formal Engineering Methods (ICFEM'05), Manchester, U.K., November 2005. Ali-Reza Adl-Tabatabai, Brian Lewis, Vijay Menon, Brian Murphy, Bratin Saha. Compiler and runtime support for software transactional memory. In Proceedings of ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation (PLDI 06), pages 26-37, Ottawa, CA, June 2006. Emery Berger and Benjamin Zorn, DieHard: Probabilistic memory safety for unsafe languages, In the Proceedings of the ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), pages: 158 - 168, June 2006. Brian Bershad, et. al. Extensibility, Safety and Performance in the SPIN Operating System. In Proceedings of the 15th ACM Symposium on Operating System Principles (SOSP-15), pp. 267-284, Copper Mountain, CO, 1995. Colin Blundell, E Christopher Lewis, Milo Martin. Deconstructing transactions: the subtleties of atomicity. In 4th Annual Workshop on Duplicating, Deconstructing and Debunking, June 2005. Hans Boehm, Towards a Memory Model for C++, lecture presentation, Redmond, WA. June 2006. Brian D. Carlstrom, JaeWoong Chung, Christos Kozyrakis, Kunle Olukotun, The software stack for transactional memory: challenges and opportunities, 1st Workshop on Software Tools for Multicore Systems (STMCS) at CGO-4, New York, NY, March, 2006. Subhachandra Chandra and Peter M. Chen, The Impact of Recovery Mechanisms on the Likelihood of Saving Corrupted State. In Proc. International Symposium on Software Reliability Engineering (ISSRE), pages: 91-101, Annapolis, MD, USA, 2002. J. Condit, M. Harren, S. McPeak, G. Necula, and W. Weimer. CCured in the real world. In Proceedings of the ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI 2003), pp. 232--244, San Diego, CA, June 2003. Peter J. Denning. Virtual Memory. In ACM Computing Surveys, 2(3), pp. 153-189. September 1970. Armando Fox and Eric Brewer. Harvest, Yield, and Scalable Tolerant Systems. In Proceedings of Hot Topics in Operating Systems (HotOS99), pages: 174-178, 1999. Arnold K, Gosling J. The Java Programming Language. Addison-Wesley--Longman: Reading, MA, 1996. D. Grossman, G. Morrisett, T. Jim, M. Hicks, Y.Wang, and J. Cheney. Region-based memory management in Cyclone. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation (PLDI 2002), pp 282293, NY, USA, 2002. ACM Press. Tim Harris, Mark Plesko, Avraham Shinnar, David Tarditi, Optimizing memory transactions. In PLDI '06: ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, pages14-25, Ottawa, CA, June 2006 Tim Harris, Keir Fraser. Language Support for Lightweight Transactions Object-Oriented Programming, Systems, Langauges & Applications (OOPSLA '03), pp 388-402, October. 2003. M.P. Herlihy and J.E.B. Moss. Transactional Memory: architectural support for lock-free data structures. In Proceedings of the International Symposium on Computer Architecture (ISCA03), San Diego, CA, May 1993. B. Hindman and D. Grossman, Strong Atomicity for Java Without Virtual-Machine Support, UW-CSE Technical Report 2006-05-01, University of Washington, 2006. Galen C. Hunt, et al., An Overview of the Singularity Project, Microsoft Research Technical Report MSR-TR-2005-135, Microsoft Corporation, Redmond, WA, Oct 2005. T. Jim, J. G. Morrisett, D. Grossman, M. W. Hicks, J. Cheney, and Y. Wang. Cyclone: A safe dialect of C. In Proceedings of the General Track: 2002 USENIX Annual Technical Conference, pages 275288, Berkeley, CA, USA, 2002. USENIX Association. P.H. Kamp. Malloc(3) revisited, http://phk.freebsd.dk/pubs/malloc.pdf. Yossi Lev, Jan-Willem Mason, Towards a safer interaction with transactional memory by tracking object visibility. In SCOOL05: Workshop on Synchronization and concurrency in Object Oriented Languages, October 2005. Microsoft Corporation. Phoenix compiler infrastructure. http://research.microsoft.com/phoenix, April 2005. G. C. Necula, S. McPeak, and W. Weimer. CCured: type-safe retrofitting of legacy code. Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming language (POPL 02), pp 128139, New York, NY, USA, 2002. ACM Press. I. Pechtchanski, V. Sarkar, Immutability Specification and its Applications, Proceedings of thee 2002 Joint ACM-ISCOPE Conference on Java Grande, pp 202-211, Seattle, WA, 2002. ACM Press. F. Quin, J. Tucek, J. Sundaresan, and Y.Y Zhou, Rx: treating bugs as allergies---a safe method to survive software failures, Proceedings of the twentieth ACM symposium on Operating Systems Principles (SOSP), pages: 238-245,Brighton, UK, 2006. M. Rinard, C. Cadar, D. Dumitran, D. M. Roy, and T. Leu. A dynamic technique for eliminating buffer overflow vulnerabilities (and other memory errors). In Proceedings of the 2004 Annual Computer Security Applications Conference (ASAC), pp. 82-90, Turscon, AZ, Dec. 2004. M. Rinard, C. Cadar, D. Dumitran, D. M. Roy, T. Leu, and J. William S. Beebee. Enhancing server availability and security through failure-oblivious computing. In Sixth Symposium on Operating Systems Design and Implementation, San Francisco, CA, Dec. 2004. USENIX. Martin Rinard, Cristian Cadar, Daniel Dumitran, Daniel Roy, Tudor Leu, and William Beebee Jr. Enhancing server availability and security through failure-oblivious computing. In Proc. Operating System Design & Implementation (OSDI), pages 303-316, 2004. Margo Seltzer, Yasuhiro Endo, Christopher Small, Keith Smith. Dealing with Disaster: Surviving Misbehaved Kernel Extensions. In Proceedings of the 1996 Symposium on Operating System Design and Implementation (OSDI II), pp. 213-227, Seattle, WA, 1996. Avraham Shinnar, David Tarditi, Mark Plesko, and Bjarne Steensgaard. Integrating support for undo with exception handling. Technical Report MSR-TR-2004-140, Microsoft Corporation, December, 2004. S. Sidiroglou, G. Giovanidis, and A. Keromytis. Using execution transactions to recover from buffer overflow attacks. Technical Report CUCS-031-04, Columbia University Computer Science Department, September 2004. Michael M. Swift, Brian N. Bershad, and Henry M. Levy. Improving the Reliability of Commodity Operating Systems In ACM Transactions on Computer Systems (TOCS), pp. 22(4), Nov. 2004. Chandramohan A. Thekkath and Henry M. Levy. Hardware and software support for efficient exception handling. In Proceedings of the 6th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS-VI , pages 110-119, October 1994. A. Troelsen, C# and the .NET Platform,, Apress, Berkeley CA, 2001 R. Wahbe, S. Lucco, T. E. Anderson, and S. L. Graham. Efficient software-based fault isolation. In Proceedings of the 14th ACM Symposium on Operating Systems Principles (SOSP), pages 203--216, December 1993. Emmett Witchel, Josh Cates, and Krste Asanovic. Mondrian memory protection. In Tenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS-X) , San Jose, CA, October 2002. Karthik Pattabiraman, Vinod Grover, and Benjamin Zorn. Samurai Protecting Critical Heap Data in Unsafe Languages. Microsoft Research Tech Report #XXX, Microsoft Corporation, Redmond, WA. August 2006. ( HYPERLINK "http://research.microsoft.com/~zorn" http://research.microsoft.com/~zorn)  Due to the floating-point nature of the Sum variable, the actual comparison consisted of checking if it was within a narrow, permissible range compared to the correct computation.     PAGE  PAGE 2 PAGE   PAGE 7 BC - @ A [ i j s иЬuj_WOWh`uOJQJh=qOJQJhEZhEZOJQJhz5CJOJQJhEjhz5CJOJQJhhzCJhhz5 hz5 hzCJ hf!2CJ huHhzhuHhz5OJQJhhz5OJQJh\nhz5OJQJhz5OJQJh~-5OJQJhhz5OJQJhuHhz5CJ hz5CJ ABCX5kd$$Ifl@ 4 la ytV $ $If^gdV$ $ p]p^a$gdzOD_  - @ { | } ~    <gd\n<gd<gd<gdz$ & F $ p]pa$gdz$ $ p]p^a$gdzs t z { | } ~   " # 5 ˺naSB1B hEZhseCJOJQJmHsH hEZhCJOJQJmHsHhs>CJOJQJmHsHh\nh\nCJOJQJ hEZh\nCJOJQJmHsHh\nCJOJQJmHsH hEZh\nCJOJQJmH sH hCJOJQJmH sH hCJOJQJmH sH  hEZhCJOJQJmH sH h\nCJOJQJmH sH hsehseCJaJhseCJaJhpxh=qOJQJh68OJQJ # 6 7 8 9 : ; D ,z3 !!"%xgdtgdnaxgdnagd$a$ $<a$gd\n<gdp<gd5 6 7 8 9 ; C D  1 - 6 <  | +$CNU»|x|h;hhhth h=_!hhuhes5ha8,hhGoh7Lh$hnah%hpx hpx5CJhuHhpxmHsHhuHhMB@mHsHhuHhpx@mHsHhuHh\nmHsHhseCJOJQJmHsH/ /Ibhkl%Hyzgh23¾ٶjh Uh hmhyhs>hCNPjNh*,UhGojhGoUhw@&h;hi2jh?Uh1dh~-jTh?Uh0jh0UhZ3hht62?h|~7:BC\]^_`¾ºº֧岺֔岺օ֐jh?Uh1)jBh?UhRhjh?Ujh0UhNlhKohZ3hCNPh-hyhw@&h0jHh71Uh~-jh Ujh71Uh 4   / 0 1 2 3 f g h !!)!G!_!b!!!!!!!!" "`"""f#v###h$i$j$$𳯷䫷𷻧hjhUhXh`uhZh h]+hExh hhwhpx hhhZFjh?Uh~-j<h?Uh0jh0Uhh1)hs>hNl4$$$$$$$$$$$% %%%v&w&&&&&&&&&&&&&&&&L'''P(`()#))2*Q*M+N+O+Z+[+Ž轹轹ŔŐ͐}v hihy hihMh$h$vh h1dhXj*h?Ujh?Uj0h?Uh0jh0UhS hwhhZh`ujh?Uhh~-jhUj6h?U.%'O+..\47:=>>>>>$Ifgdl l#E$gd0gd~gdwgdigd [+\+^+_+x+y+++++<.=.s.t...../*/?/`////)0q0000Z4[4\4555556 666 6.6/6l6s6666666 h(6 hq56hph6 hIt6hx8hIth7Nhkh6h h6h$vhhwhs>h$h~-hijhih?Ujhihy U hihy hihM466677 7 7U8t888y9999999999;:V:j:k:l:::::::::;';U<a<==> >>>>>1>2>3>9>Ų䮪ѪjhrUh0jh0UhRh( hUzqhhhhh~-j$h*,UhHjhHUhGoh$hY*hEx h$Sh~h~ h6hph6 h(6 hFY619>:>;><>=>C>D>Y>Z>[>\>>>>>>>@AAA8A9A:A=A>A?AAAAABBBBBBBBBBCCC'C+C.C/CeCfCvC~CCCCCCCDѾɺ涮 hyhx8 hx856 hx85hyhx85jhx8Uhx8h~-j h71Ujhs>Uhs>h$hph5 h5hh0jh0Uh~-mHnHu:>>>>J?q^^^$Ifgdl l#Ekd $$IflF .? t06    44 laJ?K?Z?h??q^^^$Ifgdl l#Ekd $$IflF .? t06    44 la???@H@q^^^$Ifgdl l#Ekd $$IflF .? t06    44 laH@I@X@j@@q^^^$Ifgdl l#Ekd $$IflF .? t06    44 la@@@@AAq^^^$Ifgdl l#Ekd $$IflF .? t06    44 laAABASAaAAq^^^$Ifgdl l#Ekd $$IflF .? t06    44 laAAAAEBq^^^$Ifgdl l#Ekdw $$IflF .? t06    44 laEBFBVBhBBq^^^$Ifgdl l#Ekd $$IflF .? t06    44 laBBBCCCqkVVV$Ifgd[l#G$gdx8kdk $$IflF .? t06    44 laCC'C/CfCq\\\$Ifgd[l#kd $$IflFF~ .8 t06    44 lafCgCvCCCq\\\$Ifgd[l#kd_$$IflFF~ .8 t06    44 laCCCCDq\\\$Ifgd[l#kd$$IflFF~ .8 t06    44 laDD%D6D7DtDuD~DDDDDDDDDFF{G|GGGGGGGGGMHHHJJJJJJJJJJJKK&K'K(K)K,Kοzhk5hF.B5 h(5 h'56hyh'5 h'5j>h71Ujhs>Uh'hs>h~-mHnHuh~-jh*KUjh*KUhx8h*K6h6deh*K6h*KhGohx8 hx856 hyhx80DD%D7DuDq\\\$Ifgd[l#kdS$$IflFF~ .8 t06    44 lauDvD~DDDq\\\$Ifgd[l#kd$$IflFF~ .8 t06    44 laDDDGGJJKKqlle`KKK$Ifgd[l#Ggdhgds>gd*KkdG$$IflFF~ .8 t06    44 laKKKK'K(KIkd$$Ifl\T  t0644 la$Ifgd[l#G,K4K7K8KDKEKFKLKMKYKZK`KaKhKiKnKoKpKKKKKKKKKKKKKKK L LLLMMMNNjOONPQaQ/S0SmTTUUU'UtU׬ӨӨӤӨӜhG(hMbVh*KhBrhhnh*hExh|AUhk5h~-mHnHujhs>Uhs> h'56 hyhF.BhF.Bh' hF.B56hk5h'5 h(5hk5hF.B5hk5hk556(K7KEKLKYK`KhKoKpKqKwKxKKKKKKKKKKKKKKKKK$Ifgd[l#KKK LMNP0SUHC>>>>gdhgds>kd/$$Ifl\T  t0644 la$$Ifgds>l#U'UWXYYY/Y@YJYKYYnkd $$IfTl n t0644 laytAT$$Ifgds>l#$IfgdAl#gdAcgdMbV tUUUUUUUWWGXXXXXXXXXXXXIYJYKYRYSYiYjYkYlYnYYYZZZZ'[@[V[[[e[t[u[v[w[x[[[迷Ĥ脋||||h$hH h|}h|}h2;h:Vhs>mHnHuhs>mHnHujhs>Uhs> hAc56hKcChAc5 hAc5h~-mHnHuh~-jh71UhO+jhO+UhAch|}hG(hhh]Fht0KYYZ]aaavcce3ijjIkllllll0mټĵ٭٩٥ق{wh hMB`hMB`hMB`h~-jbh*,UhGojhGoUha8,hT!nhTjh~haq haqhaqhdh6 h6hMbVh7 h6h7hh6mHnHuhuh6mHnHuhmHnHu-AލːI E;Eס/I]xgd>Zgdg & Fgdg x`gdMB`xgdMB`gdxgdgdMbV>A MiÒĒŒȒɒΒגْؒƕߕ'6 &09M쾺춮춮캟¶¶h@Y hMB`hMB`hMhM6h~h~6h~hMB`ha8,hT!nj\h?Uh~-jh?Ujh=UhuhMh h 6h h==FGߙEFJW`io;ġȡԡ֡סCl.s/<ީ #0Ѫت2HI\]ŭɽͭhO+ hh>Zh>ZhMh5VhMB`h ch7hTh.hh]h hMB`hMB`h|}h}hghaqh=hTjhT!nh@Y@]u*Oz2Hл¾)6OGgdZgd>ZgdO+$gd&gd&gd>Z x`gd>Zxgd>ZŭJKLefgklm )6Ds@yܲݲX[+-.efhPIh&6 hPIh& h&6h&hKh]4h>Z6h|}jVh71Uh jh Uh~-jh?Uh,jh,UhO+h0h>Z6 h]4h>Z h>Z6h>Z6'*cf12mn%GH\]stu|}~#غܺOPXYϻлμ¾үҾүҾ hPIh>ZhKhj/hY%KUhT!nh~-j/hY%KUh>Z h.wh>Zh~-mHnHujh&Ujh.wh>ZUjh&0JU h&6hPIh&6h&6μϼм׼ؼټKLv'A[\rst{|}ɾʾ+,BCDKLM)56O۵ߩߩױh hpxhhZUh>ZmHnHujh>ZUh>Zj1hh>ZUhKj0h?UjhT!nUhT!nh&h~-mHnHuh~-jh&Uj 0h&U3de~-./346$%>?@DEbc|}~ԺԯԤԙԎj;@h?Uj?h?UjA?h?Uj>h?UjG>h?Uh oWj=h?UhF jhF Uh@~23;<EFST[\jxyǷǤNjvh<hw6CJhVhVCJaJhwhw6CJ]h<hw6CJH*]h<hw6CJ] hwCJ\hk+hwCJ\ hwCJhk+hwCJh h 6CJ]h 6CJ]hk+h CJhk+h 6CJ] h CJ-PRUZ[!4w VW[µvk_hlDPh 6CJaJhk+h CJaJh h 6CJ] h CJh h 0J(6CJ]hk+h 6CJ]hk+h CJh 0J(CJaJhk+h 0J(CJaJh_#&h_#&6CJ]hlDPh_#&6CJ]hlDPh_#&CJ] h_#&CJ]hk+h_#&CJ]h_#&h CJaJ% {~JLWX^_o${|ᳪ~tkᛤah<h#'6CJhZhZCJhk+h#'CJ]hk+h#'6CJ] h#'CJ\hk+h#'CJ\hk+h#'CJ h#'CJhk+hZCJhwh CJ h CJh?@ABCD^`νȹ쯩؂hpxh,Vhjh?6Uh?6'*+,567BCDEFGHIJKL$a$gd,V&`#$h]hgd#' &`#$gd#'!$a$gds>LMNOPQRSTUVWXYZ[\]^_`$a$gd_#&5 0&P:p#'/ =!8"8#$% 9 0&P:p/ =!8"8#$% P 9 0&P:p\n/ =!8"8#$% P 3 0&P/ =!8"8#$% P 9 0&P:p / =!8"8#$% P R$$If !vh5#v:V l54a ytV}DyK _Ref141839313}DyK _Ref141839284}DyK _Ref141867858}DyK _Ref141874299}DyK _Ref141873972}DyK _Ref141839077}DyK _Ref141839086}DyK _Ref141839103}DyK _Ref141839119}DyK _Ref141839133}DyK _Ref141846463}DyK _Ref141846561}DyK _Ref141839313}DyK _Ref141839284}DyK _Ref141839724}DyK _Ref141851789}DyK _Ref141871592}DyK _Ref139344027x$$If!vh5?55 #v?#v#v :V#l t65?55 ax$$If!vh5?55 #v?#v#v :V#l t65?55 ax$$If!vh5?55 #v?#v#v :V#l t65?55 ax$$If!vh5?55 #v?#v#v :V#l t65?55 ax$$If!vh5?55 #v?#v#v :V#l t65?55 a}DyK _Ref141872536x$$If!vh5?55 #v?#v#v :V#l t65?55 ax$$If!vh5?55 #v?#v#v :V#l t65?55 ax$$If!vh5?55 #v?#v#v :V#l t65?55 ax$$If!vh5?55 #v?#v#v :V#l t65?55 ax$$If!vh5585 #v#v8#v :V#l t65585 ax$$If!vh5585 #v#v8#v :V#l t65585 ax$$If!vh5585 #v#v8#v :V#l t65585 ax$$If!vh5585 #v#v8#v :V#l t65585 ax$$If!vh5585 #v#v8#v :V#l t65585 ax$$If!vh5585 #v#v8#v :V#l t65585 a}DyK _Ref139344059}DyK _Ref141872870r$$If!vh5555#v#v:V#l t655ar$$If!vh5555#v#v:V#l t655a}DyK _Ref141872887V$$If!vh5n #vn :V#l t65n aytAT}DyK _Ref140403887}DyK _Ref142213393}DyK _Ref142214247}DyK _Ref142214307$$If!vh5n #vn :V#l t065n ayt T}DyK _Ref141874355}DyK _Ref141846747}DyK _Ref141846869}DyK _Ref141874299}DyK _Ref141846898}DyK _Ref141773608}DyK _Ref141842750}DyK _Ref141777394}DyK _Ref141777394}DyK _Ref141846898}DyK _Ref141777394$$If!vh5E#vE:V#l t065EaT$$If!vh5E#vE:V#l t065EaT$$If!vh5E#vE:V#l t065EaT}DyK _Ref141777394}DyK _Ref141867858}DyK _Ref140320328}DyK _Ref141841481}DyK _Ref141842408}DyK _Ref141873972>Dd r$0  # A" ?Mj" Y @= ?Mj" YYofZB\x\ pV>w<$ZA F"1A("%RH t;H@-Lh:-R3ZG|TLࣣ`uAց߹do 7srw;{~gw"EDyqD*j;8hP'Rf Dd bys}O)ʀܕ  c?g-º3!{Yn+.Mm _:ʍsl%8mXB.R{[[[| 0A )u[҄>y Bg?J09H8 '7u0+gs$E!!!c©)iSTAoНDwǴCX[^Znv״ŻzWD %jhM9S7d&JSOPS@,ۨz.U^AQ⼹.AFɛeEkm& Qo  P^#rk7Jf3ʵ)C}@QO`ZeM9yfS>qj]2JtOQWGjx)N(u!?tl Ѷ3E?ǰx2#vd'mUcu&|5 eb|H F)7tgB~]ID'-_UW xL2gQDU%\sNm5x7R%yj >0zx{׭AjLur-7qoD;>N4@IƟETOIMU jZ[\M'IvA^[H 텍&)IlAkyBi:{=cQY:-5x ZCV_ZYe@C,.yzEmbqʫrX\^ N~ (=e"y>f@yh,.y܃޿pP.z ]WŲEcq"|ȵ墟1bq(1XKzɖzzqLT) "yƊetn*IAR&ϱBg P.U>Ku/z jLlD.u>K_J,.;.ripkP4}S rk^z!X/m-|oS|πT{?H)Cl)$˷-5*WeDJb WFWcFJ b!WVWgEJb[!W¯W^_O~{_)M4_O~_)-4q~J;*U8 ӿ_u;*pe7P 1ep (_8lHN@7Q &B ʯ'Yo,HI@W*ViBʯ'Jw JHU@W-5ՀӣV (:j3:pzj!u_mkVi(&_8FHS@,Z05CZ/e9v,{ډH8 <~soɈ2xYEdo8 L޹ocI "ZNh- mqi/yT u𷻩rN0ޟN0REtk঍Tp̓U~1 bYoJM8/VۿT_(罹= ]˦b).vyYtJfy}[:}ۇݫ=>&v}̇k,ݰeWcQ첝ᰫ~/rN/Φ>Z,ϫ%8e{u>/^sXmsK8/gɴ;w?b㨋}"6fuG}LU$:F KvU;7J]0w̠BKYgb_?ٰAWNs/Ei;zeױ:>"mu:֗C:KVkT+ݙ3 ߹P>:GMK8Iς>^?lё򙈷4Q(C\D}hY6OެBUl[M>N2 {By{!r>?]"G}aF?Stx -_k3\~.iiQ-㑾z+/A-"l1.T6kELz%t0H9VxsgĆSׇW,K}5+8?#EzںmS;HgS¶j{O]x M:N~hU6=R1̇_!!Gkdn4R1 I620RK|`=fjg͕~~.~[sF=(Zd^ UJ-ݜמʚZWUPh{$i_ /Ƿ{bPulϻ{fտ{۳![jڮ!ۦy{ۃ.mZc}emz)m쮴}6{ީlOkZ'rwd^%>I6eϳ|L2.=c޷v^/zo~ὁ.?/we>7sg={ݽ2~ kDhgJhz1QAQ6YOP(e40 vc ?tm&+mKۻJ/(MǀGJSN]K(Jaooo%?pY9:ڶՅD6fff(҂*T=Ҏ>&hs1M^{:DtFy!z@x`+@olyFzVb̫{tĒ0Ⱓ/ ~"GМ'Žo=f4v4Lާ/?E/vҩŃO&)tuf=)ĴgQ>5^Q]əf;*!;?xL`cXf{1K}{%hgK_u̺?Wo/5t_ʺ1y>hsOiL9ӗv:gи"Ypn\oڍlo xL^vO_1l,gbl,|WTOen7=n M)K>s\xf!,^ߕ*QY#a.j* 5j.1i_>YFOs"e/F"}HG~{Vo9QhVGꌯ>so[,|/Iv0iۯ൶F>En?Sc؃~w#4U=i=co[-|>z —SW#&$;- gx.~_mW[~~d3~J 9у|OϳVX )^E9.QHV@1VGT4mh3!zNtu@SWO?sjepBU:Bzd =O.&Be.mC_&t'ԵCJruUhhE.;ş[uJKltAg/AgBgǠ]]'Չ- AgYt5Ag1phΚѶ%7D 7E p R-W3ՌvNj}A_1 jއy~qE.ftk2NkK6WX2t5ku}5ǚ5wR}9e8 ȸ5A5;lZʨcAw2j?s5>'2d;O3Ya,}'ձ'q~rr{ 45{V31n!Gdи1'c-˳9VBZ|f *wN\I Ui3mB;$K:/NYAI3%ϴy"gho5yu\OHX2nR;dsዀèD<4N%e -> $&#(}]~}xԵC}E>(}Х>>J.}cG4nkS/{צM4.=S~K0n;|`Z5>yY"ݼ+ZF4+֏pl檯#[AgTq9L-6V~qRURWAʽU^~Qbg/x%O6"}oxrKMg~p;Mkvϋ;}˝i6{ 智׽eHnFX'en}u7\M ~)r.Ўr@ d5Njݜnuo#ͱ ;@|4Ȗ㮐97{:TE,ȗ?qJ >5Q#;H)JEgw+M]n]}yǺɻ{l/{-㦫T0y\v3oFmZ/u7򒋚bAB0(eߍ}DyK _Ref141773619}DyK _Ref141864876}DyK _Ref141848067}DyK _Ref141848089}DyK _Ref141848155}DyK _Ref141848157}DyK _Ref141848159}DyK _Ref140403887}DyK _Ref141873972}DyK _Ref141874299}DyK _Ref141842729}DyK _Ref141842533}DyK _Ref141842549}DyK _Ref141842750}DyK _Ref141849676}DyK _Ref141840914}DyK _Ref141839313}DyK _Ref140318656}DyK _Ref140403887}DyK _Ref140404365}DyK _Ref141871592}DyK _Ref141871628}DyK _Ref140320328}DyK _Ref141871663}DyK _Ref140320309}DyK _Ref140404623}DyK _Ref141851815DyK $http://research.microsoft.com/~zornyK `http://research.microsoft.com/~zornyX;H,]ą'c%,F@F Normal $Pa$CJ_HmH sH tH V@V Heading 1$$ & F(@&a$ 5CJKH8@8 Heading 2  & F@&B@!B Heading 3  & F@& 56CJ8@18 Heading 4  & F@&^@^ Heading 5*$ & F(@&^`a$6CJT@T Heading 6 & F<@&6CJOJQJkHL@L Heading 7 & F<@& OJQJkHP@P Heading 8 & F<@&6OJQJkHT @T Heading 9 & F<@&6CJOJQJkHDA@D Default Paragraph FontVi@V  Table Normal :V 44 la (k(No List P&@P Footnote ReferenceCJH*OJQJkH>O> Author$a$CJOJQJkHPOP Paper-Title $xa$5CJ$OJQJkHFO"F Affiliations$a$ CJOJQJJ@2J  Footnote Textp^`pCJOB Bulletp & Fp>Th^`p4 @R4 Footer  !,Ob, E-Mail<LOrL Abstract$ & Fx@& a$5CJ;@ List Number 3p & F8>Th.^8`POP Captions$H#$+Dp/0$a$5CJ>O> References$ & Fa$.)@. Page NumberHC@H Body Text Indenth`hRYR  Document Map-D M OJQJ^JB"@B Caption$a$5\^JaJtH TB@T Body Text#/H&#$+D@/0$CJ6U@6 Hyperlink >*B*ph4@4 Header ! !<P@"<  Body Text 2 "dx|@3|  Table Grid<:V#0a #$Pa$_HHBH .k Balloon Text$CJOJQJ^JaJB'QB .kComment ReferenceCJaJ8b8 .k Comment Text&CJ@jab@ .kComment Subject'5\O m.X@. Emphasis6]ROR F references *$ hh^h`a$aJFV@F 9FollowedHyperlink >*B* ph` `                |~7;`7r789:;D&?'M'jˈ ]uO6Oa@0@0@0@0@00  0  0A 099A 099A 099A 099 @ 0A 0--@08A 0--A 0-- @ 0A 0--@08 @ 0A 0--A 0--00hC ABCX-@{|}~#6789:;D, z3O#&&\,/2=66666666J7K7Z7h77778H8I8X8j88888A9B9S9a99999E:F:V:h::::;;;;';/;f;g;v;;;;;;<<%<7<u<v<~<<<<<??BBCCCCC'C(C7CECLCYC`ChCoCpCqCwCxCCCCCCCCCCCCCCCCCCC DENH0KM'MOPQQQ/Q@QJQKQQRUYYYv[[]3abbIcdddddd0eD,KtU[sf;tFzɀ>ŭμcM  ` %>J??H@@AAAEBBCfCCDuDDK(KKUKY?@ABCEDFGHIbnn,,48??d;; ]aax|mppa  !"#$%&'()*+,-./0123465789:<;=>?@ABCEDFGHI >B*urn:schemas-microsoft-com:office:smarttags PostalCode:F*urn:schemas-microsoft-com:office:smarttagsStreet=H*urn:schemas-microsoft-com:office:smarttags PlaceName9C*urn:schemas-microsoft-com:office:smarttagsState=I*urn:schemas-microsoft-com:office:smarttags PlaceType;G*urn:schemas-microsoft-com:office:smarttagsaddress8D*urn:schemas-microsoft-com:office:smarttagsCityB8*urn:schemas-microsoft-com:office:smarttagscountry-region9J*urn:schemas-microsoft-com:office:smarttagsplace>>*urn:schemas-microsoft-com:office:smarttags PersonName y`JIHGFJDCBJDJ>DJCDJ8DJCDJCJDJCDJC8DJDJCJ8DJCDJCIJHDJCDJC8DJDJC8DJ8DJCJDCDJC  "#5    a$n$'*';&;g;u;;;<$<<<CCCCC%C(C4C7C=C`CeC|CCP QQQQ,Q4Q?QUU`%```dd4e9e@eDeqrlsssssssssuuwww wfwlwqwxwxxRxVxixqxxx~~"0AP̈́ڄމ/9Ί׊'6ӐNRw{ip2:il7B{eqQW&"#(*/DK"$)*/16KR(-=CDH9@ #$, 9?,34;W`pw,27=NT"'-   .4".2:8@]czhmnvO    CDa"#5^^aabbjjYlZl~~GOil7Cgl QW!/O    CDa333333333333333333333333XXkgB`3giv^##k226;6C6\69>9::{??BBCCPPRQlQV&VrZZr^^{jjKklk;ll!oBo~qq.rPrrruu||B}d}Ɋ؊Kl m\~ٴ[}ɶ+Md4$Eb?`y:z BciEfjMmXy Q(N    ),47ACDaO    CDa ? v:K)>\A4]KpRgZH( `)^3 C.v0j;q69yDz~'nF( K~H yrJz3PB TN{5a!jocq?mgyƲ< |h,@.@.@..@...@ ....@ .....@ ......@ .......@ ........^`o(. ^`hH. pLp^p`LhH. @ @ ^@ `hH. ^`hH. L^`LhH. ^`hH. ^`hH. PLP^P`LhH.hhh^h`OJQJo(hHh88^8`OJQJ^Jo(hHoh^`OJ QJ o(hHh  ^ `OJQJo(hHh  ^ `OJQJ^Jo(hHohxx^x`OJ QJ o(hHhHH^H`OJQJo(hHh^`OJQJ^Jo(hHoh^`OJ QJ o(hHh^`OJQJo(hHh^`OJQJ^Jo(hHohpp^p`OJ QJ o(hHh@ @ ^@ `OJQJo(hHh^`OJQJ^Jo(hHoh^`OJ QJ o(hHh^`OJQJo(hHh^`OJQJ^Jo(hHohPP^P`OJ QJ o(hH^`OJPJQJ^Jo(-^`OJQJ^Jo(hHopp^p`OJ QJ o(hH@ @ ^@ `OJQJo(hH^`OJQJ^Jo(hHo^`OJ QJ o(hH^`OJQJo(hH^`OJQJ^Jo(hHoPP^P`OJ QJ o(hH@.@.@..@...@ ....@ .....@ ......@ .......@ ........h88^8`OJ QJ o(hHh^`OJQJ^Jo(hHoh  ^ `OJ QJ o(hHh  ^ `OJQJo(hHhxx^x`OJQJ^Jo(hHohHH^H`OJ QJ o(hHh^`OJQJo(hHh^`OJQJ^Jo(hHoh^`OJ QJ o(hH^`6CJOJQJo(. ^`hH. pLp^p`LhH. @ @ ^@ `hH. ^`hH. L^`LhH. ^`hH. ^`hH. PLP^P`LhH.hhh^h`56o(hH.h 88^8`hH.h L^`LhH.h   ^ `hH.h   ^ `hH.h xLx^x`LhH.h HH^H`hH.h ^`hH.h L^`LhH.h^`OJQJo(hHh^`OJQJ^Jo(hHohpp^p`OJ QJ o(hHh@ @ ^@ `OJQJo(hHh^`OJQJ^Jo(hHoh^`OJ QJ o(hHh^`OJQJo(hHh^`OJQJ^Jo(hHohPP^P`OJ QJ o(hH^`CJOJQJo(^`CJOJQJo(opp^p`CJOJ QJ o(@ @ ^@ `CJOJ QJ o(^`CJOJ QJ o(^`CJOJ QJ o(^`CJOJ QJ o(^`CJOJ QJ o(PP^P`CJOJ QJ o(h88^8`OJ QJ o(hHh^`OJQJ^Jo(hHoh  ^ `OJ QJ o(hHh  ^ `OJQJo(hHhxx^x`OJQJ^Jo(hHohHH^H`OJ QJ o(hHh^`OJQJo(hHh^`OJQJ^Jo(hHoh^`OJ QJ o(hHh^`OJQJo(hH ^`hH. pLp^p`LhH. @ @ ^@ `hH. ^`hH. L^`LhH. ^`hH. ^`hH. PLP^P`LhH.@.@.@..@...@ ....@ .....@ ......@ .......@ ........h^`56hH)h ^`hH.h pLp^p`LhH.h @ @ ^@ `hH.h ^`hH.h L^`LhH.h ^`hH.h ^`hH.h PLP^P`LhH.@.@.@..@...@ ....@ .....@ ......@ .......@ ........@.@.@..@...@ ....@ .....@ ......@ .......@ ........hh^h`6CJOJQJo([]hh^h`o() 88^8`hH. L^`LhH.   ^ `hH.   ^ `hH. xLx^x`LhH. HH^H`hH. ^`hH. L^`LhH.h^`OJPJQJ^Jo(hH-hzz^z`OJQJ^Jo(hHohJJ^J`OJ QJ o(hHh  ^ `OJQJo(hHh  ^ `OJQJ^Jo(hHoh^`OJ QJ o(hHh^`OJQJo(hHhZZ^Z`OJQJ^Jo(hHoh**^*`OJ QJ o(hH^`o(. ^`hH. pLp^p`LhH. @ @ ^@ `hH. ^`hH. L^`LhH. ^`hH. ^`hH. PLP^P`LhH.!joZHnFgy]K!jo JyK~Hz3P C. )>\j;q6Kcq |? `)yDTgyrJN{5a                          w                 %                                                    Z#        4b         9,:m1W1#S-1#fZ>D%(V2kd1#h[-\04ZF`ksZHlS=k1n"pZT 8Z l   - F n y K Z ei ,Ohv(9muA-Ig9,H9D!:I7:l;<;%;-;2;</<Va<~<n=>>v>>~2?u@|@*7@AF.BMBPWBKcC=D`DpfD~E3E:EnE]F G GGVGuHb)JKKY%K<-LjLjNDN7N>O~PlDPCNPQ!S;S=SkT+T-hT-U/U|AUFVMbV&xV.W%W=W oW!X_X@YhY*Z>ZEZ[[\\S]U].^h^#^(^MB`X`y`naWb5%b4jb=c%=]^^a$ cmWdm/H^'e\@u?WsetpD%MWZ1pO,)U|l1d]w'js<3xvT%\FH4|}|SU,V= ^9? 1)#,6^2RuK^-4JAc*p2BV zMNpVfhn G(AVi*7Lw ,>}~'L{t687c"e+{,\:k )+z^!4/q5@P ?6ER.02Ee^h Mb5fT* I${~hj8pUq7[R6V${idR%&t;KQxx$aK&opc 9qpm|BC6666666J7K7Z7h77778H8I8X8j88888A9B9S9a99999E:F:V:h::::;;;;';/;f;g;v;;;;;;<<%<7<u<v<~<<<<BBCC'C(CoCCCCCPJQKQdJeKewxxzz||a@\\research\113S4thDNe07:winspool\\research\113S4thD\\research\113S4thD S odXXLetterPRIV0''''\i_+\IUPHdLetter o [none] [none]4Pd?ZORN44dMicrosoft Office WordWINWORD.EXEC:\Program Files\Microsoft Office\OFFICE11\WINWORD.EXE\\research\113S4thD S odXXLetterPRIV0''''\i_+\IUPHdLetter o [none] [none]4Pd?ZORN44dMicrosoft Office WordWINWORD.EXEC:\Program Files\Microsoft Office\OFFICE11\WINWORD.EXE8S`@@Unknown S: Times New RomanTimes5SymbolG& : ArialHelveticaA& Trebuchet MS?5 z Courier New;" Helvetica3TimesA& zaTahoma?? ??U MiriamTimes New Roman;Wingdings"h FcF䧦 &')&')!4d 2qHX?p2Proceedings Template - WORDEnd User Computing ServicesBenjamin G. Zorn`                Oh+'0   <H h t  Proceedings Template - WORDEnd User Computing Services Normal.dotBenjamin G. Zorn13Microsoft Office Word@q@@Njµ@8u&')՜.+,D՜.+,H hp|  ACMd Proceedings Template - WORD Title 8@ _PID_HLINKSAvn$http://research.microsoft.com/~zorn  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~Root Entry F3Data K1Table-,WordDocumentSummaryInformation(DocumentSummaryInformation8CompObjq  FMicrosoft Office Word Document MSWordDocWord.Document.89q