Pages

Oct 15, 2010

Effortvescence: Real Reality

Effortvescence: Real Reality: "The wheel moves, the wind mill turns, words are spoken etc... So many such things appear to be the ones behind the bigger picture, like a mo..."

Oct 12, 2010

You are the Source

You are the source
You are the destination
You are the path that leads to the force

You are the light
You are the dawn
You are the spring that flows around

You are the freedom
You are the love
You are the flight of the doves

You are the justice
You are the space
You are the life of the face

You are the beauty
You are the grace
You are the strand that ties the lace

You are the fire
You are the water
You are the wind that blows

You are the death
You are the truth
You are the life that flows

Oct 5, 2010

Vultures and Swan

so you went to the vulture's nest
oh great feast you had
the fat, the black, the ugly
the aloof and the sad

they all sat on the big table
and ordered a sumptuous meal
munch munch they went on
I understand not what's the deal

unless you hunt your prey
what pleasure is there to eat
it doesn't matter if you cook
or you went out for a treat

the vultures weren't satisfied,
with the food they just had,
they were driven by greed and passion,
oh thats always the plan they had

back in the fat one's nest
they all sat together
and played the games of pleasure
among all those who gathered

through the darkness of night
across the great big sea
there was a great white swan
as caring and loving he could be

he gave away his sleep
as he waited for you alone
watching out for his beloved
and hoping the vultures be gone

oh the tragic ending
you yelled at the poor swan
you wish he would have slept
or even better just get drown

we all seem to like the vultures
as evil as they may be
no one cares for the swan
or his dark lonely song

Oct 4, 2010

Another New Poem by Dr. Kumar Vishwas

Update:
Another Latest Poem by Kumar Vishwas
Selected Stanzas from Kumar Vishwas Poems

मेरा अपना तजुर्बा है वही बतला रहा हूँ मैं
कोई लभ छू गया था तब कि अब तक गा रहा हूँ मैं
फिर आके प्यार मैं कैसे जिया जाये बिना तडपे
जो मैं खुद ही नहीं समझा वही समझा रहा हूँ मैं

कसी पत्थर मैं मूरत है कोई पत्थर कि मूरत है
लो हमने देख ली दुनिया जो इतनी खूबसूरत है
जमाना अपनी समझे पर मुझे अपनी खबर यह है
तुझे मेरी ज़जूरत है मुझे तेरी ज़रुरत है

कोई कब तक मेहेज सोचे कोई कब तक मेहेज गाये
इलाही क्या यह मुमकिन है कि कुछ ऐसा भी हो जाए
मेरा महताब उसकी रात के आहोश मैं पिघले
मैं उसकी नींद मैं जागु वोह मुझे मैं घुल के सो जाये

कोई मनजिल नहीं जचती सफ़र अच्छा नहीं लगता
अगर घर लौट भी आऊं तोह घर अच्छा नहीं लगता
कहूँ कुछ भी मैं अब दुनिया को सब अच्छा ही लगता है
मुझे कुछ भी तुम्हारे बिन मगर अच्छा नहीं लगता

Oct 3, 2010

Every act I deliver is performance

Every act I deliver is performance,
Every word I speak is speech,
Every thought I have is theory,
Every action I do is practice,
Every belief I hold is religion,
Every path I take is freedom,
Every dream I have is future,
Every darkness I see is night,
Every ray I feel is hope,
Every pain I sense is fear,
Every book I write is fact,
Every song I compose is melody,
Every idea I get is revolution,
Every sight I look is vision,
Every life I have is birth,
Every death I get is salvation.

Dr. Kumar Vishwas' s New Poem for Indians Living Abroad

हर एक कोने हर एक पाने में तेरी याद आती है
नमक आखों में घुल जाने में तेरी याद आती है
तेरी अमृत भरी लहरों क्या मालूम गंगा माँ
समंदर पार विराने में तेरी याद आती है

कहीं खाली पड़े आलिन्द तेरी याद आती है
सुबह के ख्वाब के मानिंद तेरी यार आती है
hello hey hi सुनकर तोह नही आती मगर हमसे
कोई कहता है जब जय हिंद तेरी याद आती है

सुझाए माँ जो महूरत तोह तेरी याद आती है
हँसे गर बुध की मूरत तोह तेरी याद आती है
कहीं dollar के पीछे छिप गए भारत के नोटों पर
दिखे गाँधी कि जो मूरत तोह तेरी याद आती है

- कुमार विश्वास

Oct 2, 2010

A cut-off approach for bounded verification of parameterized systems (ICSE 2010) - A Short Review

A cut-off approach for bounded verification of parameterized systems. - Qiusong Yang, Mingshu Li


In this paper a new approach based on forward bounded reachability analysis is proposed for verification of parameterized systems. Experimental results show improvements in verification efficiency as a result of introduction of new cut offs on the maximum length of paths.

For the notations used in the paper, the properties of parameterized systems are expressed in property automata, whose accepting languages (paths leading to trap states) prescribe undesirable behaviour of verified system. The overall approach starts with construction of an extended reachability graph (ERG), which is the synchronous product of the property automaton and the parameterized system. It models the execution of control processes and regulated replications of a parameterized system and their execution’s impact on the property automaton. Instead of using a complete ERG a set of increasingly refined abstractions to it is sequentially generated.  In order to abstract the global state of the parameterized system a notion of configuration is introduced as follows

-          Configuration is a vector of the form c= where ‘s’ is a state vector and ‘a’ is a counter vector.
-          These configuration form the vertices of the ERG while the edges of the graph represent the transitions between these configurations

-          It can  be shown that is possible to calculate the configurations inductively from a finite bounded ERG
The authors state and prove a theorem in the paper which shows that only a finite bounded ERG is needed in order to prove the property.

The given algorithm is implemented in java and compared with other existing algorithms for verification of parameterized systems. The results of such a comparison show that FBRA out performs the known methods in many of the examples. But in a few cases it is indeed slower which the authors attribute to the enumeration of all states in ERGs.  As future work they propose to adopt some of the strategies used to optimize the FBRA algorithm.


Falcon: fault localization in concurrent programs (ICSE 2010) - A Short Review

Falcon: fault localization in concurrent programs - Sangmin Park, Richard W. Vuduc, Mary Jean Harrold

This paper presents a new dynamic fault localization technique that can pinpoint faulty data-access patterns in multithreaded concurrent programs. The authors explain the technique by means of running example which proceedings with the following steps

-          The authors start with defining concurrency violations of interest for this paper

o   Data Race – do not focus on it in this paper but the method can handle this
o   Order Violation – Conflicting interleaving patterns
o   Atomicity Violation –  Unserializable interleaving patterns

-          Online Pattern Identification, in this step they monitor an instrumented version of the program which is run multiples times. In each of these runs a fixed sliding window is used to identify patterns. Any interesting pattern is an interleaving of read write accesses to a shared memory location. These patterns are associated with passing and failing executions.

o   Within a particular siding window look for access for a particular shared memory location
o   Once the window becomes full, scan it for unserializable interleaving patterns
o   If there is no unserializable interleaving pattern check for conflicting interleaving patterns
o   Emit all patterns found
o   These patterns are then associated with passing and failing executions

-          In the second step the patterns are ranked using suspiciousness (based on Jaccard Index) which represents the likelihood of a pattern being related to a fault.
                                                                                                
A prototype implementation (FALCON) of this technique in Java and a detailed empirical study of the system is given next in the paper. They evaluate the effectiveness and efficiency of the system with respect to the ability to indentify suspicious patterns which relate to faults. The results from the study of window size show that for most cases a moderate window (10) size can still enable FALCON to detect many relevant suspicious patterns (75%). Finally a study indirectly compares FALCON to CCI (which is a related recent work done in fault localization) the authors conclude that FALCON ranks the patterns much better than the related ranking of accesses from CCI.

Even though the initial study is promising there are a number of limitations which can form future work, current system only take 1 test input and execute the program multiple times. There is no relation between the pattern and the actual bug that causes the suspicious pattern.  A single bug may give rise to many patterns or vice versa. There are other types of violations like deadlocks which are not currently indentified using FALCON.


Oracle-guided component-based program synthesis (ICSE 2010) - A Short Review

Oracle-guided component-based program synthesis - Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, Ashish Tiwari


In this paper the authors propose a novel technique for synthesizing loop-free programs. Two potential usage of such a synthesis can be in generating efficient bit manipulating programs and for deobfuscating malware programs.  Formally the synthesis problem considered in the paper requires

-          A validation oracle V, that, given any candidate program can tell whether the program is the desired one or not. (For the examples in this paper the user herself is the validation oracle)

-          An I/O oracle I, that, given any program input, returns the output of the desired program on that input. (Again the user herself is the I/O oracle for the examples in this paper)

-          A set of specifications called a library of basic components f, such that each component includes,
o   A tuple of input variables and a output variable
o   An expression over the input and out variables such that it specifics the input-output relationship of the component

Now the goal of the synthesis problem is to synthesize a program P that can be validated by the oracle V, i.e. V (P) = true.  Further, the program P should be contrasted using only the base components in the library.
The authors propose an encoding of the program using a set of integer-valued location variables L, such that the value of the variable determine which components goes where (location) and from which location it takes its input. Next they define two constraints

-          I/O behavioural constraint which ensures that the generated program has the same input-output behaviour as that specified by the I/O oracle.

-          Distinguishing constraint which generates an input that differentiates this program from another candidate program

Now you can synthesis the candidate program by using SMT solvers to solve the behavioural constraint and then using SMT solvers again to solve the distinguishing constraint that will generate an input (new) which is added to the set of input-output pairs and this continues unless we get a semantically unique program (shown my failure of SMT solver to solve distinguishing constraint). Check that program with the validation oracle to see if it valid.

The evaluation sections shows the applicability of this approach to synthesize minimal bit manipulating programs and the authors also discuss optimizing this technique by using an application dependent bias in the sampling of input space. In the discussion the authors explore connections of this approach with fundamental results in computational learning theory.  They say that on the basis of the teaching dimension results by Goldman and Kerns it can be shown that only a few examples would be needed to synthesis these programs as they form a low teaching dimension.

Possible weakness of the approach is limitation to synthesis of simple (minimal) loop-free programs.


Has the bug really been fixed? (ICSE 2010) - A short review

This paper defines and formalizes the Bad Fix Problem, as per studies developers spend 50-80 % of their time fixing bugs. Many of these bug fixes themselves are a) sources of new bugs and b) do not fix the original bug for all inputs. The authors formalize these two notions as Coverage and Disruption.

Where,

Coverage of the fix measures the extent to which the fix correctly handles all the bug triggering inputs

And Disruption of a fix counts the deviations from the program’s intended behaviour introduced by a fix.

Hence for a given fix, the Bad Fix Problem is to determine the coverage and disruption of the fix.

The approach taken to calculate the Coverage for the fix is based on Distance Bounded Weakest Precondition (WP). In order to mitigate the path-explosion problem of WP the authors calculate the WP for a subset of paths near a distinguished path in the interprocedural control flow graph (ICFG).  The distance measure they use for nearness is the Levenshtein distance (which represents the minimum number of add/delete/substitutes required to change a string to another). The concrete path induced by the known bug triggering input is used as the distinguished path for calculating the Distance Bounded WP.

Once we have the distance bounded WP the coverage of a fix is determined by executing the Program symbolically using the WP and deriving a Post Condition (eliminating non-input variables from the clause).  For a buggy input the output of the program violates an assertion (say A) now if the post condition implies A then the fix is valid in terms of the coverage or else we report a counter example as a new bug triggering input.
The violations in disruption are defined by the test suite. So if the new Program runs on standard regression test cases as well as on a random subset of inputs we claim the fix valid and every test case failure is a disruption.

The authors implement this approach in a tool for the java language (FIXATION). The empirical evaluation shows that fixation is able to identify the known bad fixes in the code in reasonable time. The path explosion problem of WP is avoided by using a distance measure for calculating WP. The authors show that the analysis is able to scale for increasing values of distance “d”.

One of the limitations of this approach can be that it models the bugs as assertion failures and it relies on assertions being available or inferred. Also determining the value of distance “d” to obtain a better results is still a problem the papers suggests that the user start with a small value and increment it as more paths are explored. The possible future application of this approach can be in unit testing where the tool can directly work with the self contained assertions in a unit test case.

References

  1. Gu, Zhongxian, et al. "Has the bug really been fixed?." Software Engineering, 2010 ACM/IEEE 32nd International Conference on. Vol. 1. IEEE, 2010.

Short Summary of Few Papers from ICSE 2010

Naoyasu Ubayashi, Jun Nomura, Tetsuo Tamai:
Archface: a contract place where architectural design and code meet 
together.

- This paper proposes a new mechanism based on component-and-connector architecture to bridge the gap between design and implementation. The authors introduce a notion of predicate coordination where program points are exposed by a predicate and coordinated by a connector. Archface is implemented on ASPECTJ and uses AOP notions of joint points and advice to implement.


Daniel Le Mtayer, Manuel Maarek, Valrie Viet Triem Tong, Eduardo Mazza,
Marie-Laure Potet, Nicolas Craipeau, Stphane Frnot, Ronan Hardouin:
Liability in software engineering: overview of the LISE approach and 
illustration on a case study.

- This paper attempes to formalize the notion of liability and illustrates the use of formal definations by means of a running case study. The authors show how in this particular case formal methods can be used to manage legal issues and fix liability in case of a claim by the customer. There are many legal aspects regarding goverment laws, collecting evidence before claim, etc which are left out of the scope of the study, Nevertheless this paper shows how formal methods can be useful even in areas like legal liability in today's world.

Thomas D. LaToza, Brad A. Myers:
Developers ask reachability questions.

- This paper is a study of interviews taken by the author of professional developers and the kind of questions they ask while coding/debugging. The most common questions which developers seem to care about are the kind where you need to search across feasible paths through a program for target statements matching a search criterion (Reachability Question). Not many IDE support answering these kinds of questions on large complex codebases hence a lot of development time is spent (9 out of 10 longest activities).

Thomas Fritz, Gail C. Murphy:
Using information fragments to answer the questions developers ask. 

- This paper tries to use automated composition of information fragments (like who is working on what, which classes where changes since yesterday, what are my team members working on etc) to answer some of the questions developers face during their work daily. Using the information fragment model proposed by authors the developers were able to answer 94% (of 78) of commonly identified such questions. The paper evaluates it with a detailed usability study with 18 professional developers who are trained for 15 mins to use this system before evaluation.


Piramanayagam Arumuga Nainar, Ben Liblit:
Adaptive bug isolation. 

- This paper uses statistical models to instrument and monitor only those program behaviours which are predictive of failure and thus shows considerable performance improvements as compared to realistic sampling based instrumentation and complete binary instrumentation. The authors achieve this by starting with monitoring only a small portion of the program and automatically refining the instrumentation over time. This refinement is modelled as a search over the CDG of the program. The paper evaluates different heuristics and design alternatives to perform this search effectively.

Brian Demsky, Patrick Lam:
Views: object-inspired concurrency control. 

- This paper attempts to bring in a notion of views in to manage fine grained concurrency control. As claimed by the authors views make the task of implementing sophisticated locking schemes and provide static checks to avoid many kind of data races.  The evaluation section of the paper seems weak, in the sense it doesn't go beyond telling us that "they implemented views and it works". The authors conclude that in their experience working with views was simpler and easier.

Empirical Studies
----------------

Swarup Kumar Sahoo, John Criswell, Vikram S. Adve:
An empirical study of reported bugs in server software with implications 
for automated bug diagnosis. 

- A new study which looks at a sample of bugs from the 6 major open source server software. Some of the interesting results seem to be that there are very less concurrent bugs in production versions, most bugs (80%) can be reproduced by running the last input before crash/bug again. This has some implications for designing bug analysis software for such servers which they discuss in the paper.

Aditya V. Nori, Sriram K. Rajamani:
An empirical study of optimizations in YOGI.

- An empirical study of the 5 major optimizations done by the team in the new Static Verification Tool- Yogi, which is currently being evaluated by the windows group for use in static driver verifier. This is a first such attempt of trying to study the heuristics that go into building a real world tool with emphasis on the engineering efficiencies gained by using the heuristics in form of faster and more precise analysis.



New Tool for IDE
----------------

Andrew Bragdon, Steven P. Reiss, Robert C. Zeleznik, Suman Karumuri,
William Cheung, Joshua Kaplan, Christopher Coleman, Ferdi Adeputra, Joseph
J. LaViola Jr.:
Code bubbles: rethinking the user interface paradigm of integrated 
development environments.

- This paper evaluates the use of a new metaphor to view and edit large amount of code aka bubbles. The authors present usability studies and interviews with professional developers to illustrate the efficiency and productivity of using bubbles in the development process as compared to a Window/Tab based UI.