bluuebunny/crossref_metadata_2025 huggingface dataset:
Data representation synthesis
Authors: Hawkins Peter , Aiken Alex , Fisher Kathleen , Rinard Martin , Sagiv Mooly
Published: October 2012

We consider the problem of specifying combinations of data structures with complex sharing in a manner that is both declarative and results in provably correct code. In our approach, abstract data types are specified using relational algebra and functional dependencies. We describe a language of decompositions that permit the user to specify different concrete representations for relations, and show that operations on concrete representations soundly implement their relational specification. It is easy to incorporate data representations synthesized by our compiler into existing systems, leading to code that is simpler, correct by construction, and comparable in performance to the code it replaces.
Synthesizing geometry constructions
Authors: Gulwani Sumit , Korthikanti Vijay Anand , Tiwari Ashish
Published: October 2012

In this paper, we study the problem of automatically solving ruler/compass based geometry construction problems. We first introduce a logic and a programming language for describing such constructions and then phrase the automation problem as a program synthesis problem. We then describe a new program synthesis technique based on three key insights: (i) reduction of symbolic reasoning to concrete reasoning (based on a deep theoretical result that reduces verification to random testing), (ii) extending the instruction set of the programming language with higher level primitives (representing basic constructions found in textbook chapters, inspired by how humans use their experience and knowledge gained from chapters to perform complicated constructions), and (iii) pruning the forward exhaustive search using a goal-directed heuristic (simulating backward reasoning performed by humans). Our tool can successfully synthesize constructions for various geometry problems picked up from high-school textbooks and examination papers in a reasonable amount of time. This opens up an amazing set of possibilities in the context of making classroom teaching interactive.
Synthesis of loop-free programs
Authors: Gulwani Sumit , Jha Susmit , Tiwari Ashish , Venkatesan Ramarathnam
Published: October 2012

We consider the problem of synthesizing loop-free programs that implement a desired functionality using components from a given library. Specifications of the desired functionality and the library components are provided as logical relations between their respective input and output variables. The library components can be used at most once, and hence the library is required to contain a reasonable overapproximation of the multiset of the components required.

We solve the above component-based synthesis problem using a constraint-based approach that involves first generating a synthesis constraint, and then solving the constraint. The synthesis constraint is a first-order ∃∀ logic formula whose size is quadratic in the number of components. We present a novel algorithm for solving such constraints. Our algorithm is based on counterexample guided iterative synthesis paradigm and uses off-the-shelf SMT solvers.

We present experimental results that show that our tool Brahma can efficiently synthesize highly nontrivial 10-20 line loop-free bitvector programs. These programs represent a state space of approximately 20
10
programs, and are beyond the reach of the other tools based on sketching and superoptimization.
Automatic compilation of MATLAB programs for synergistic execution on heterogeneous processors
Authors: Prasad Ashwin , Anantpur Jayvant , Govindarajan R.
Published: October 2012

MATLAB is an array language, initially popular for rapid prototyping, but is now being increasingly used to develop production code for numerical and scientific applications. Typical MATLAB programs have abundant data parallelism. These programs also have control flow dominated scalar regions that have an impact on the program's execution time. Today's computer systems have tremendous computing power in the form of traditional CPU cores and throughput oriented accelerators such as graphics processing units(GPUs). Thus, an approach that maps the control flow dominated regions to the CPU and the data parallel regions to the GPU can significantly improve program performance.

In this paper, we present the design and implementation of MEGHA, a compiler that automatically compiles MATLAB programs to enable synergistic execution on heterogeneous processors. Our solution is fully automated and does not require programmer input for identifying data parallel regions. We propose a set of compiler optimizations tailored for MATLAB. Our compiler identifies data parallel regions of the program and composes them into kernels. The problem of combining statements into kernels is formulated as a constrained graph clustering problem. Heuristics are presented to map identified kernels to either the CPU or GPU so that kernel execution on the CPU and the GPU happens synergistically and the amount of data transfer needed is minimized. In order to ensure required data movement for dependencies across basic blocks, we propose a data flow analysis and edge splitting strategy. Thus our compiler automatically handles composition of kernels, mapping of kernels to CPU and GPU, scheduling and insertion of required data transfer. The proposed compiler was implemented and experimental evaluation using a set of MATLAB benchmarks shows that our approach achieves a geometric mean speedup of 19.8X for data parallel benchmarks over native execution of MATLAB.
EnerJ
Authors: Sampson Adrian , Dietl Werner , Fortuna Emily , Gnanapragasam Danushen , Ceze Luis , Grossman Dan
Published: October 2012

Energy is increasingly a first-order concern in computer systems. Exploiting energy-accuracy trade-offs is an attractive choice in applications that can tolerate inaccuracies. Recent work has explored exposing this trade-off in programming models. A key challenge, though, is how to
isolate parts of the program that must be precise from those that can be approximated
so that a program functions correctly even as quality of service degrades.

We propose using type qualifiers to declare data that may be subject to approximate computation. Using these types, the system automatically maps approximate variables to low-power storage, uses low-power operations, and even applies more energy-efficient algorithms provided by the programmer. In addition, the system can statically guarantee isolation of the precise program component from the approximate component. This allows a programmer to control explicitly how information flows from approximate data to precise data. Importantly, employing static analysis eliminates the need for dynamic checks, further improving energy savings. As a proof of concept, we develop EnerJ, an extension to Java that adds approximate data types. We also propose a hardware architecture that offers explicit approximate storage and computation. We port several applications to EnerJ and show that our extensions are expressive and effective; a small number of annotations lead to significant potential energy savings (10%-50%) at very little accuracy cost.
A case for an SC-preserving compiler
Authors: Marino Daniel , Singh Abhayendra , Millstein Todd , Musuvathi Madanlal , Narayanasamy Satish
Published: October 2012

The most intuitive memory consistency model for shared-memory multi-threaded programming is
sequential consistency
(SC). However, current concurrent programming languages support a relaxed model, as such relaxations are deemed necessary for enabling important optimizations. This paper demonstrates that an SC-preserving compiler, one that ensures that every SC behavior of a compiler-generated binary is an SC behavior of the source program, retains most of the performance benefits of an optimizing compiler. The key observation is that a large class of optimizations crucial for performance are either already SC-preserving or can be modified to preserve SC while retaining much of their effectiveness. An SC-preserving compiler, obtained by restricting the optimization phases in LLVM, a state-of-the-art C/C++ compiler, incurs an average slowdown of 3.8% and a maximum slowdown of 34% on a set of 30 programs from the SPLASH-2, PARSEC, and SPEC CINT2006 benchmark suites.

While the performance overhead of preserving SC in the compiler is much less than previously assumed, it might still be unacceptable for certain applications. We believe there are several avenues for improving performance without giving up SC-preservation. In this vein, we observe that the overhead of our SC-preserving compiler arises mainly from its inability to aggressively perform a class of optimizations we identify as
eager-load
optimizations. This class includes common-subexpression elimination, constant propagation, global value numbering, and common cases of loop-invariant code motion. We propose a notion of
interference checks
in order to enable eager-load optimizations while preserving SC. Interference checks expose to the compiler a commonly used hardware speculation mechanism that can efficiently detect whether a particular variable has changed its value since last read.
Toward generating reducible replay logs
Authors: Lee Kyu Hyung , Zheng Yunhui , Sumner Nick , Zhang Xiangyu
Published: October 2012

Logging and replay is important to reproducing software failures and recovering from failures. Replaying a long execution is time consuming, especially when replay is further integrated with runtime techniques that require expensive instrumentation, such as dependence detection. In this paper, we propose a technique to reduce a replay log while retaining its ability to reproduce a failure. While traditional logging records only system calls and signals, our technique leverages the compiler to selectively collect additional information on the fly. Upon a failure, the log can be reduced by analyzing itself. The collection is highly optimized. The additional runtime overhead of our technique, compared to a plain logging tool, is trivial (2.61% average) and the size of additional log is comparable to the original log. Substantial reduction can be cost-effectively achieved through a search based algorithm. The reduced log is guaranteed to reproduce the failure.
Finding and understanding bugs in C compilers
Authors: Yang Xuejun , Chen Yang , Eide Eric , Regehr John
Published: October 2012

Compilers should be correct. To improve the quality of C compilers, we created Csmith, a randomized test-case generation tool, and spent three years using it to find compiler bugs. During this period we reported more than 325 previously unknown bugs to compiler developers. Every compiler we tested was found to crash and also to silently generate wrong code when presented with valid input. In this paper we present our compiler-testing tool and the results of our bug-hunting study. Our first contribution is to advance the state of the art in compiler testing. Unlike previous tools, Csmith generates programs that cover a large subset of C while avoiding the undefined and unspecified behaviors that would destroy its ability to automatically find wrong-code bugs. Our second contribution is a collection of qualitative and quantitative results about the bugs we have found in open-source C compilers.
Evaluating value-graph translation validation for LLVM
Authors: Tristan Jean-Baptiste , Govereau Paul , Morrisett Greg
Published: October 2012

Translation validators are static analyzers that attempt to verify that program transformations preserve semantics. Normalizing translation validators do so by trying to match the value-graphs of an original function and its transformed counterpart. In this paper, we present the design of such a validator for LLVM's intra-procedural optimizations, a design that does not require any instrumentation of the optimizer, nor any rewriting of the source code to compile, and needs to run only once to validate a pipeline of optimizations. We present the results of our preliminary experiments on a set of benchmarks that include GCC, a perl interpreter, SQLite3, and other C programs.
Safe optimisations for shared-memory concurrent programs
Authors: Ševčík Jaroslav
Published: October 2012

Current proposals for concurrent shared-memory languages, including C++ and C, provide sequential consistency only for programs without data races (the DRF guarantee). While the implications of such a contract for hardware optimisations are relatively well-understood, the correctness of compiler optimisations under the DRF guarantee is less clear, and experience with Java shows that this area is error-prone.

In this paper we give a rigorous study of optimisations that involve both reordering and elimination of memory reads and writes, covering many practically important optimisations. We first define powerful classes of transformations semantically, in a language-independent trace semantics. We prove that any composition of these transformations is sound with respect to the DRF guarantee, and moreover that they provide basic security guarantees (no thin-air reads) even for programs with data races. To give a concrete example, we apply our semantic results to a simple imperative language and prove that several syntactic transformations are safe for that language. We also discuss some surprising limitations of the DRF guarantee.
Systematic editing
Authors: Meng Na , Kim Miryung , McKinley Kathryn S.
Published: October 2012

Software modifications are often
systematic
---they consist of similar, but not identical, program changes to multiple contexts. Existing tools for systematic program transformation are limited because they require programmers to manually prescribe edits or only suggest a location to edit with a related example. This paper presents the design and implementation of a program transformation tool called SYDIT. Given an example edit, SYDIT generates a
context-aware, abstract edit script
, and then applies the edit script to new program locations. To correctly encode a relative position of the edits in a new location, the derived edit script includes unchanged statements on which the edits are control and data dependent. Furthermore, to make the edit script applicable to a new context using different identifier names, the derived edit script abstracts variable, method, and type names. The evaluation uses 56 systematic edit pairs from five large software projects as an oracle. SYDIT has high coverage and accuracy. For 82% of the edits (46/56), SYDIT matches the context and applies an edit, producing code that is 96% similar to the oracle. Overall, SYDIT mimics human programmers correctly on 70% (39/56) of the edits. Generation of edit scripts seeks to improve programmer productivity by relieving developers from tedious, error-prone, manual code updates. It also has the potential to guide automated program repair by creating program transformations applicable to similar contexts.
A security policy oracle
Authors: Srivastava Varun , Bond Michael D. , McKinley Kathryn S. , Shmatikov Vitaly
Published: October 2012

Even experienced developers struggle to implement security policies correctly. For example, despite 15 years of development, standard Java libraries still suffer from missing and incorrectly applied permission checks, which enable untrusted applications to execute native calls or modify private class variables without authorization. Previous techniques for static verification of authorization enforcement rely on manually specified policies or attempt to infer the policy by code-mining. Neither approach guarantees that the policy used for verification is correct.

In this paper, we exploit the fact that many modern APIs have
multiple, independent
implementations. Our flow- and context-sensitive analysis takes as input an API, multiple implementations thereof, and the definitions of security checks and security-sensitive events. For each API entry point, the analysis computes the security policies enforced by the checks before security-sensitive events such as native method calls and API returns, compares these policies across implementations, and reports the differences. Unlike code-mining, this technique finds missing checks even if they are part of a rare pattern. Security-policy differencing has no intrinsic false positives: implementations of the same API
must
enforce the same policy, or at least one of them is wrong!

Our analysis finds 20 new, confirmed security vulnerabilities and 11 interoperability bugs in the Sun, Harmony, and Classpath implementations of the Java Class Library, many of which were missed by prior analyses. These problems manifest in 499 entry points in these mature, well-studied libraries. Multiple API implementations are proliferating due to cloud-based software services and standardization of library interfaces. Comparing software implementations for consistency is a new approach to discovering "deep" bugs in them.
Language-independent sandboxing of just-in-time compilation and self-modifying code
Authors: Ansel Jason , Marchenko Petr , Erlingsson Úlfar , Taylor Elijah , Chen Brad , Schuff Derek L. , Sehr David , Biffle Cliff L. , Yee Bennet
Published: October 2012

When dealing with dynamic, untrusted content, such as on the Web, software behavior must be sandboxed, typically through use of a language like JavaScript. However, even for such specially-designed languages, it is difficult to ensure the safety of highly-optimized, dynamic language runtimes which, for efficiency, rely on advanced techniques such as Just-In-Time (JIT) compilation, large libraries of native-code support routines, and intricate mechanisms for multi-threading and garbage collection. Each new runtime provides a new potential attack surface and this security risk raises a barrier to the adoption of new languages for creating untrusted content.

Removing this limitation, this paper introduces general mechanisms for safely and efficiently sandboxing software, such as dynamic language runtimes, that make use of advanced, low-level techniques like runtime code modification. Our
language-independent sandboxing
builds on Software-based Fault Isolation (SFI), a traditionally static technique. We provide a more flexible form of SFI by adding new constraints and mechanisms that allow safety to be guaranteed despite runtime code modifications.

We have added our extensions to both the x86-32 and x86-64 variants of a production-quality, SFI-based sandboxing platform; on those two architectures SFI mechanisms face different challenges. We have also ported two representative language platforms to our extended sandbox: the Mono common language runtime and the V8 JavaScript engine. In detailed evaluations, we find that sandboxing slowdown varies between different benchmarks, languages, and hardware platforms. Overheads are generally moderate and they are close to zero for some important benchmark/platform combinations.
Automated atomicity-violation fixing
Authors: Jin Guoliang , Song Linhai , Zhang Wei , Lu Shan , Liblit Ben
Published: October 2012

Fixing software bugs has always been an important and time-consuming process in software development. Fixing concurrency bugs has become especially critical in the multicore era. However, fixing concurrency bugs is challenging, in part due to non-deterministic failures and tricky parallel reasoning. Beyond correctly fixing the original problem in the software, a good patch should also avoid introducing new bugs, degrading performance unnecessarily, or damaging software readability. Existing tools cannot automate the whole fixing process and provide good-quality patches.

We present AFix, a tool that automates the whole process of fixing one common type of concurrency bug: single-variable atomicity violations. AFix starts from the bug reports of existing bug-detection tools. It augments these with static analysis to construct a suitable patch for each bug report. It further tries to combine the patches of multiple bugs for better performance and code readability. Finally, AFix's run-time component provides testing customized for each patch. Our evaluation shows that patches automatically generated by AFix correctly eliminate six out of eight real-world bugs and significantly decrease the failure probability in the other two cases. AFix patches never introduce new bugs and usually have similar performance to manually-designed patches.
NDSeq
Authors: Burnim Jacob , Elmas Tayfun , Necula George , Sen Koushik
Published: October 2012

We propose to specify the correctness of a program's parallelism using a sequential version of the program with controlled nondeterminism. Such a
nondeterministic sequential specification
allows (1) the correctness of parallel interference to be verified independently of the program's functional correctness, and (2) the functional correctness of a program to be understood and verified on a sequential version of the program, one with controlled nondeterminism but no interleaving of parallel threads.

We identify a number of common patterns for writing nondeterministic sequential specifications. We apply these patterns to specify the parallelism correctness for a variety of parallel Java benchmarks, even in cases when the functional correctness is far too complex to feasibly specify.

We describe a sound runtime checking technique to validate that an execution of a parallel program conforms to its nondeterministic sequential specification. The technique uses a novel form of conflict-serializability checking to identify, for a given interleaved execution of a parallel program, an equivalent nondeterministic sequential execution. Our experiments show a significant reduction in the number of false positives versus traditional conflict-serializability in checking for parallelization bugs.
Cause clue clauses
Authors: Jose Manu , Majumdar Rupak
Published: October 2012

Much effort is spent by programmers everyday in trying to reduce long, failing execution traces to the
cause
of the error. We present an algorithm for error cause localization based on a reduction to the maximal satisfiability problem (MAX-SAT), which asks what is the maximum number of clauses of a Boolean formula that can be simultaneously satisfied by an assignment. At an intuitive level, our algorithm takes as input a program and a failing test, and comprises the following three steps. First, using bounded model checking, and a bound obtained from the execution of the test, we encode the semantics of a bounded unrolling of the program as a Boolean
trace formula
. Second, for a failing program execution (e.g., one that violates an assertion or a post-condition), we construct an
unsatisfiable
formula by taking the formula and additionally asserting that the input is the failing test and that the assertion condition does hold at the end. Third, using MAX-SAT, we find a maximal set of clauses in this formula that can be satisfied together, and output the complement set as a potential cause of the error.

We have implemented our algorithm in a tool called BugAssist that performs error localization for C programs. We demonstrate the effectiveness of BugAssist on a set of benchmark examples with injected faults, and show that in most cases, BugAssist can quickly and precisely isolate a few lines of code whose change eliminates the error. We also demonstrate how our algorithm can be modified to automatically suggest fixes for common classes of errors such as off-by-one.We have implemented our algorithm in a tool called BugAssist that performs error localization for C programs. We demonstrate the effectiveness of BugAssist on a set of benchmark examples with injected faults, and show that in most cases, BugAssist can quickly and precisely isolate a few lines of code whose change eliminates the error. We also demonstrate how our algorithm can be modified to automatically suggest fixes for common classes of errors such as off-by-one.
Kremlin
Authors: Garcia Saturnino , Jeon Donghwan , Louie Christopher M. , Taylor Michael Bedford
Published: October 2012

Many recent parallelization tools lower the barrier for parallelizing a program, but overlook one of the first questions that a programmer needs to answer:
which parts of the program should I spend time parallelizing
?

This paper examines Kremlin, an automatic tool that, given a serial version of a program, will make recommendations to the user as to what regions (e.g. loops or functions) of the program to attack first. Kremlin introduces a novel
hierarchical critical path analysis
and develops a new metric for estimating the potential of parallelizing a region:
self-parallelism
. We further introduce the concept of a
parallelism planner
, which provides a ranked order of specific regions to the programmer that are likely to have the largest performance impact when parallelized. Kremlin supports multiple
planner personalities
, which allow the planner to more effectively target a particular programming environment or class of machine.

We demonstrate the effectiveness of one such personality, an OpenMP planner, by comparing versions of programs that are parallelized according to Kremlin's plan against third-party manually parallelized versions. The results show that Kremlin's OpenMP planner is highly effective, producing plans whose performance is typically comparable to, and sometimes much better than, manual parallelization. At the same time, these plans would require that the user parallelize significantly fewer regions of the program.
Automatic parallelization via matrix multiplication
Authors: Sato Shigeyuki , Iwasaki Hideya
Published: October 2012

Existing work that deals with parallelization of complicated reductions and scans focuses only on formalism and hardly dealt with implementation. To bridge the gap between formalism and implementation, we have integrated parallelization via matrix multiplication into compiler construction. Our framework can deal with complicated loops that existing techniques in compilers cannot parallelize. Moreover, we have sophisticated our framework by developing two sets of techniques. One enhances its capability for parallelization by extracting max-operators automatically, and the other improves the performance of parallelized programs by eliminating redundancy. We have also implemented our framework and techniques as a parallelizer in a compiler. Experiments on examples that existing compilers cannot parallelize have demonstrated the scalability of programs parallelized by our implementation.
Verification of semantic commutativity conditions and inverse operations on linked data structures
Authors: Kim Deokhwan , Rinard Martin C.
Published: October 2012

We present a new technique for verifying
commutativity conditions
, which are logical formulas that characterize when operations commute. Because our technique reasons with the abstract state of verified linked data structure implementations, it can verify commuting operations that produce semantically equivalent (but not necessarily identical) data structure states in different execution orders. We have used this technique to verify sound and complete commutativity conditions for all pairs of operations on a collection of linked data structure implementations, including data structures that export a set interface (ListSet and HashSet) as well as data structures that export a map interface (AssociationList, HashTable, and ArrayList). This effort involved the specification and verification of 765 commutativity conditions.

Many speculative parallel systems need to undo the effects of speculatively executed operations.
Inverse operations
, which undo these effects, are often more efficient than alternate approaches (such as saving and restoring data structure state). We present a new technique for verifying such inverse operations. We have specified and verified, for all of our linked data structure implementations, an inverse operation for every operation that changes the data structure state.

Together, the commutativity conditions and inverse operations provide a key resource that language designers, developers of program analysis systems, and implementors of software systems can draw on to build languages, program analyses, and systems with strong correctness guarantees.
Exploiting the commutativity lattice
Authors: Kulkarni Milind , Nguyen Donald , Prountzos Dimitrios , Sui Xin , Pingali Keshav
Published: October 2012

Speculative execution is a promising approach for exploiting parallelism in many programs, but it requires efficient schemes for detecting conflicts between concurrently executing threads. Prior work has argued that checking semantic commutativity of method invocations is the right way to detect conflicts for complex data structures such as kd-trees. Several ad hoc ways of checking commutativity have been proposed in the literature, but there is no systematic approach for producing implementations.

In this paper, we describe a novel framework for reasoning about commutativity conditions: the commutativity lattice. We show how commutativity specifications from this lattice can be systematically implemented in one of three different schemes: abstract locking, forward gatekeeping and general gatekeeping. We also discuss a disciplined approach to exploiting the lattice to find different implementations that trade off precision in conflict detection for performance. Finally, we show that our novel conflict detection schemes are practical and can deliver speedup on three real-world applications.
On inter-procedural analysis of programs with lists and data
Authors: Bouajjani Ahmed , Drăgoi Cezara , Enea Constantin , Sighireanu Mihaela
Published: October 2012

We address the problem of automatic synthesis of assertions on sequential programs with singly-linked lists containing data over infinite domains such as integers or reals. Our approach is based on an accurate abstract inter-procedural analysis. Program configurations are represented by graphs where nodes represent list segments without sharing. The data in these list segments are characterized by constraints in abstract domains. We consider a domain where constraints are in a universally quantified fragment of the first-order logic over sequences, as well as a domain constraining the multisets of data in sequences.

Our analysis computes the effect of each procedure in a local manner, by considering only the reachable part of the heap from its actual parameters. In order to avoid losses of information, we introduce a mechanism based on unfolding/folding operations allowing to strengthen the analysis in the domain of first-order formulas by the analysis in the multisets domain.

The same mechanism is used for strengthening the sound (but incomplete) entailment operator of the domain of first-order formulas. We have implemented our techniques in a prototype tool and we have shown that our approach is powerful enough for automatic (1) generation of non-trivial procedure summaries, (2) pre/post-condition reasoning, and (3) procedure equivalence checking.
Taming the wildcards
Authors: Altidor John , Huang Shan Shan , Smaragdakis Yannis
Published: October 2012

Variance allows the safe integration of parametric and subtype polymorphism. Two flavors of variance, definition-site versus use-site variance, have been studied and have had their merits hotly debated. Definition-site variance (as in Scala and C#) offers simple type-instantiation rules, but causes fractured definitions of naturally invariant classes; Use-site variance (as in Java) offers simplicity in class definitions, yet complex type-instantiation rules that elude most programmers.

We present a unifying framework for reasoning about variance. Our framework is quite simple and entirely denotational, that is, it evokes directly the definition of variance with a small core calculus that does not depend on specific type systems. This general framework can have multiple applications to combine the best of both worlds: for instance, it can be used to add use-site variance annotations to the Scala type system. We show one such application in detail: we extend the Java type system with a mechanism that modularly infers the definition-site variance of type parameters, while allowing use-site variance annotations on any type-instantiation.

Applying our technique to six Java generic libraries (including the Java core library) shows that 20-58 (depending on the library) of generic definitions are inferred to have single-variance; 8-63% of method signatures can be relaxed through this inference, and up to 91% of existing wildcard annotations are unnecessary and can be elided.
Synchronization via scheduling
Authors: Best Micah J. , Mottishaw Shane , Mustard Craig , Roth Mark , Fedorova Alexandra , Brownsword Andrew
Published: October 2012

Shared state access conflicts are one of the greatest sources of error for fine grained parallelism in any domain. Notoriously hard to debug, these conflicts reduce reliability and increase development time. The standard task graph model dictates that tasks with potential conflicting accesses to shared state must be linked by a dependency, even if there is no explicit logical ordering on their execution. In cases where it is difficult to understand if such
implicit
dependencies exist, the programmer often creates more dependencies than needed, which results in constrained graphs with large monolithic tasks and limited parallelism.

We propose a new technique, Synchronization via Scheduling (SvS), that uses the results of static and dynamic code analysis to manage potential shared state conflicts by exposing the data accesses of each task to the scheduler. We present an in-depth performance analysis of SvS via examples from video games, our target domain, and show that SvS performs well in comparison to software transactional memory (TM) and fine grained mutexes.
An Interview with Sebastian Deterding
Authors: Bozarth Jane
Published: October 2012

Researcher and UX designer Sebastian Deterding, who specializes in persuasive design and gameful design discusses "gamification," intrinsic motivation, and good game design.
Using Skype as an Academic Tool: Lessons Learned
Authors: Sivula Martin
Published: October 2012

Inside or outside the traditional or virtual classroom, Skype is a proven academic software tool. Instructors and students can communicate freely regardless of location, creating unrestricted convenience and strengthening personal interactions.
Meeting the challenges of rising enrollments
Authors: Roberts Eric S.
Published: October 2012

FOR MOST OF THE LAST DECADE, the number of computer science majors declined signifi cantly at colleges and universities throughout the United States, in spite of continuing demand from industry for graduates in the fi eld. In the last few years, however, many institutions have witnessed a dramatic turnaround in enrollment, with many more students choosing to become CS majors, or at least exploring that possibility by taking introductory computer science courses.
A computer perspective
Authors: Randell Brian
Published: October 2012

This anecdote concerns the preparation of a revised edition of the book "A Computer Perspective", by the late Charles and Ray Eames, a book whose first edition was produced in 1973 to accompany the IBM History Wall exhibit. The revised edition was reproduced photographically from the original plates in 1990, when the plates were found after being lost for many years, with a rewritten introduction and epilogue.
The game of elevenses
Authors: Rolfe Timothy J.
Published: October 2012

It is becoming increasingly diffi cult to develop programming assignments for which the students cannot fi nd implementations on-line. This article describes a fairly simple game for which at the moment this is not the case. It is a card game based on scoring face cards and pairs of non-face cards totaling eleven.
A virtual tutor for relational schema normalization
Authors: Yang Feng-Jen
Published: October 2012

The idea of virtualization has been successfully practiced in many fi elds of information technology such as the virtualizations of operating systems, memories, networks, and even human tutors. This research is a virtualization of human tutoring in the domain of relational database schema normalization implemented as an intelligent tutoring system usable as a virtual tutor to facilitate the knowledge acquisition of relational database schema normalization.
A study on the cognitive style of software developers
Authors: Rui Deng , Wei She , Li Zhao , Hong Yang
Published: October 2012

Excellent software developers displayed outstanding colony characteristics in the cognitive style. It's assumed that the software developers preferred certain dimensions of the cognitive style, and then four specific sub-tests are defined after the modification according to Riding's testing mode named Cognitive Style Analysis System. Testees were divided into Group A (software developers) and Group B (common testees). The system recorded the score and reaction time of the testees for each test during the survey. The studies show that, compared to the common testees, software developers' verbal/imagery dimension of the cognitive style belongs to the significant imagery preference. As to wholist/analytic dimension, software developers are wholist style but non-significant.
Affecting attitudes in first-year computer science using syntaxfree robotics programming
Authors: Anderson Monica , McKenzie Andrew , Wellman Briana , Brown Marcus , Vrbsky Susan
Published: October 2012

Persistence of first-year students in computer science is a problem. Although there are many factors that determine whether a student can be successful in computer science, research has shown that some attrition is due to personal perception of their ability in computer science. We created a learning experience specifically designed to improve students' self-assessment of their abilities. "Providing robotic experiences through objectbased programming" (PREOP) is a GUI programming environment based on Alice that students use to program autonomous robot controllers. Results show that for students that rate themselves as average programmers, the modules designed around PREOP positively affect the students' intimidation levels.
Teaching problem solving effectively
Authors: Hasni Tahreem Fatima , Lodhi Fakhar
Published: October 2012

To teach students problem solving effectively it is important to guide them properly through the process of problem solving. Most of the programming lab exercises lack emphasis on practicing the process of problem solving. Based on our experience, we have suggested a guideline to design lab exercises. In which we emphasize on defining detailed steps to guide students through the process of problem solving. We have proven through experiments that lab exercises designed with guidelines provided to solve the problem are very effective way of teaching problem solving skills.
Mind the (gender) gap
Authors: Eidelman Larisa , Hazzan Orit , Lapidot Tami , Matias Yossi , Raijman Daniela , Segalov Michal
Published: October 2012

This paper presents the "Mind the Gap" initiative that aims to encourage female high school pupils to study computer science (CS) in high school. This is achieved by increasing their awareness to what CS is, and exposing them to the essence of a hi-tech environment and to same gender role models. Female software engineers at Google's Israel R&D Center in collaboration with the Israeli National Center undertook the initiative for computer science teachers. We describe the initiative and its impact on the female pupils' interest in CS. One of our conclusions is that even a short visit to a hi-tech company, in this case - Google, has the potential to change pupils' perception of what CS is and to increase their interest in CS and their desire to study it. One could easily adapt this initiative to other companies and scale it to infl uence a rather large population.
Exponential base change based on symmetry
Authors: Rolfe Timothy
Published: October 2012

This article examines the recurrence obtained for Catalan numbers based on their description of the number of unique binary search tree structures possible with
n
distinct keys. The straightforward recurrence obtained, when transformed into a recursive method, obtains the solution in 3

n

method invocations. With a small change based on symmetry, this can be changed to obtain the solution in 2

n

method invocations. Of course, one can obtain the solution in massively fewer operations (O(
n
2
)) in a dynamic programming/memoized solution.
A special type-independent programming approach using available underlying constructs in a programming language
Authors: Danesh Iraj
Published: October 2012

Facilities such as templates, STL, and Boost libraries are popular sources for generic programming and present a high-level view of the machine to the students of programming. The approach presented in this paper emphasizes on a different method of type independent programming that presents a lower-level view of the machine to the students. The merit of this approach is that students will gain some insight into the implementation of generics and better understand the underlying constructs available to them. Programming in this task becomes innovative and more challenging and enriches in-debt knowledge of the students in underlying layers in certain courses of computer science, and potentially contributes to computing education. Prospective C++ built-in constructs (other than templates) were studied to obtain their feasibility of how each or a combination of them can be employed to write data-type independent programs. Several code segments were developed and tested to confirm the genericness and applicability of each of them individually or as a combination.
Fifty years of automata simulation
Authors: Chakraborty Pinaki , Saxena P. C. , Katti C. P.
Published: October 2012

Automata theory is an important subject in computer science and quite consequently, simulation of automata for pedagogical purposes is an important topic in computer science education research. This article reviews the major initiatives in the field of simulation of automata in the last five decades with emphasis on those automata simulators actually used at universities for teaching. A classification of the automata simulators on the basis of their design paradigms has been developed where they have been classified broadly into language based automata simulators and visualization centric automata simulators. Some salient trends in the research on simulation of automata are also identified. The article concludes with an advocacy for continuing research on simulation of automata and integration of automata simulators in teaching.
ACM copyrights and plagiarism
Authors: Walker Henry M.
Published: October 2012

As authors consider forums for publication, some common questions involve copyright: Who owns the copyright? May I post a copy of my piece on the Web? Could I publish the material in another publication?
Trial by Fire: Lessons Learned in Developing and Delivering A Distance Learning Course
Authors: Faught Charie
Published: October 2012

The purpose of the article is to present first-hand experience of developing distance delivery courses, including technical and course development considerations. The article provides practical considerations into the use of distance delivery tools for combining the live classroom experience and includes challenges and lessons learned.
Top Tools for Learning
Authors: Hart Jane
Published: October 2012

In Jane Hart's new monthly column for eLearn Magazine, she shares some "gems": useful or valuable tools, resources, and products she has unearthed for learning and performance improvement/support. In this month's column she focuses on new tools for learning.
Five Expectations Students Should Have of an Online Instructor
Authors: Ely Sabrina
Published: October 2012

In recent years, online degree programs have become a widely accepted modality for many learners who are seeking a college degree. Online learning is a great choice for a student who is a self-motivated, and who are independent learners. This article will share five of the best tips to help your online students succeed.
Writing (And Reading) Conference Session Descriptions
Authors: Quinn Clark
Published: October 2012

You should be thinking about presenting at a conference, but you need several things: an appropriate topic for the audience, a good presentation, and a compelling description to send to the conference organizers. In this article, consultant and semi-professional conference presenter Clark Quinn covers knowing your audience, knowing what makes an engaging session, and knowing what organizers are looking for.
If Mobile Learning and Support are Wonderful, Why aren't They Everywhere?
Authors: Rossett Allison
Published: October 2012

Although we hear many expressions of enthusiasm for mobile learning and support, there isn't a lot of documented activity, not yet. This article describes possibilities and focuses on figuring out why it is not yet happening. What gets in the way of the use of mobile devices for learning, support, and community?
Why Is the Research on Learning Styles Still Being Dismissed by Some Learning Leaders and Practitioners?
Authors: Wallace Guy W.
Published: October 2012

A learning style is supposedly a mode of learning that is most effective for an individual. It supposedly helps to improve learning results. Why does this myth persist? Twenty-five years of research on this and related themes have not provided any form of conclusive evidence that matching the form of instruction to learning style improved learning or even attention.
Book Review: 'Designing mLearning' by Clark Quinn
Authors: Silvers Aaron
Published: October 2012

mLearning is not about a full-fledged mobile-based platform to use for every learning situation; rather, mLearning is to augment, expand and/or bridge gaps in learning activities offered through many other means.
Are Students Tuning You Out or Downloading You In? Improving Online Instruction for 21st Century Skills
Authors: Levin-Goldberg Jennifer
Published: October 2012

In the past five years, online learning has augmented significantly. However, the question is, with this increased proliferation in its popularity, has online learning been authentically preparing students for 21st century skills? According to a myriad of statistics and studies, the dismal response is no. Recognizing the mounting interest in online education and whether or not schools are genuinely equipping and priming students for 21st century skills, this article suggests five strategies to not only improve the online learning experience, but to integrate and polish students for the 21st century with skills requisite to capitalize upon for global success.
Book Review: 'Design for How People Learn (Voices That Matter)' by Julie Dirksen
Authors: Unrein Judy
Published: October 2012

eLearn Magazine contributor Judy Unrein checks out Julie Dirksen's "Design for How People Learn," and finds it both a solid primer for beginners and an excellent reframe for experienced instructional designers.
Are Virtual Worlds (still) Relevant in Education?
Authors: Smith-Robbins Sarah
Published: October 2012

We have seen the idea of virtual worlds in education run the gamut of reactions over the last few years. From early unknowns, to excitement, to evangelism and early adopters, and to today's somewhat jaded and cautious reactions, virtual worlds in education have been a hotly debated topic. So, we ask, are virtual worlds still relevant in education? Have they ever been? Will they be in the future?
Book Review: 'E-Learning Provocateur; Volume 1'
Authors: Bickford Alison
Published: October 2012

In his book, Ryan Tracey provides the learning professional with thought provoking insights into the role of learning technologies in organizational learning, and the part we are charged with in ensuring technology enables and does not impede staff learning and performance.