| 1. |
- Abbas, Qaisar, et al.
(author)
-
Energy Stability of the MUSCL Scheme
- 2010
-
In: Proc. 7th South African Conference on Computational and Applied Mechanics. - Berlin : South African Association for Theoretical and Applied Mechanics. ; , s. 65:1-8, s. 61-68
-
Conference paper (other academic/artistic)
|
|
| 2. |
- Abbas, Qaisar, 1975-
(author)
-
Weak Boundary and Interface Procedures for Wave and Flow Problems
- 2011
-
Doctoral thesis (other academic/artistic)abstract
- In this thesis, we have analyzed the accuracy and stability aspects of weak boundary and interface conditions (WBCs) for high order finite difference methods on Summations-By-Parts (SBP) form. The numerical technique has been applied to wave propagation and flow problems.The advantage of WBCs over strong boundary conditions is that stability of the numerical scheme can be proven. The boundary procedures in the advection-diffusion equation for a boundary layer problem is analyzed. By performing Navier-Stokes calculations, it is shown that most of the conclusions from the model problem carries over to the fully nonlinear case.The work was complemented to include the new idea of using WBCs on multiple grid points in a region, where the data is known, instead of at a single point. It was shown that we can achieve high accuracy, an increased rate of convergence to steady-state and non-reflecting boundary conditions by using this approach.Using the SBP technique and WBCs, we have worked out how to construct conservative and energy stable hybrid schemes for shocks using two different approaches. In the first method, we combine a high order finite difference scheme with a second order MUSCL scheme. In the second method, a procedure to locally change the order of accuracy of the finite difference schemes is developed. The main purpose is to obtain a higher order accurate scheme in smooth regions and a low order non-oscillatory scheme in the vicinity of shocks.Furthermore, we have analyzed the energy stability of the MUSCL scheme, by reformulating the scheme in the framework of SBP and artificial dissipation operators. It was found that many of the standard slope limiters in the MUSCL scheme do not lead to a negative semi-definite dissipation matrix, as required to get pointwise stability.Finally, high order simulations of shock diffracting over a convex wall with two facets were performed. The numerical study is done for a range of Reynolds numbers. By monitoring the velocities at the solid wall, it was shown that the computations were resolved in the boundary layer. Schlieren images from the computational results were obtained which displayed new interesting flow features.
|
|
| 3. |
|
|
| 4. |
- Abdulhadi, Nadia M. Noor, et al.
(author)
-
Doctors' and nurses' views on patient care for type 2 diabetes : an interview study in primary health care in Oman
- 2013
-
In: Primary Health Care Research and Development. - : Cambridge University Press. - 1463-4236 .- 1477-1128. ; 14:3, s. 258-269
-
Journal article (peer-reviewed)abstract
- Aim: This study aimed at exploring the experiences of primary health-care providers of their encounters with patients with type 2 diabetes, and their preferences and suggestions for future improvement of diabetes care. Background: Barriers to good diabetes care could be related to problems from health-care providers' side, patients' side or the healthcare system of the country. Treatment of patients with type 2 diabetes has become a huge challenge in Oman, where the prevalence has increased to high levels. Method: Semi-structured interviews were conducted with 26 health-care professionals, 19 doctors and seven nurses, who worked in primary health care in Oman. Qualitative content analysis was applied. Findings: Organizational barriers and barriers related to patients and healthcare providers were identified. These included workload and lack of teamwork approach. Poor patients' management adherence and influence of culture on their attitudes towards illness were identified. From the providers' side, language barriers, providers' frustration and aggressive attitudes towards the patients were reflected. Decreasing the workload, availability of competent teams with diabetes specialist nurses and continuity of care were suggested. Furthermore, changing professional behaviours towards a more patient-centred approach and need for health education to the patients, especially on self-management, were addressed. Appropriate training for health-care providers in communication skills with emphasis on self-care education and individualization of care according to each patient's needs are important for improvement of diabetes care in Oman.
|
|
| 5. |
- Abdulla, Parosh Aziz, et al.
(author)
-
An Integrated Specification and Verification Technique for Highly Concurrent Data Structures
- 2013
-
In: Tools and Algorithms for the Construction and Analysis of Systems. - Berlin, Heidelberg : Springer Berlin Heidelberg.
-
Conference paper (peer-reviewed)abstract
- We present a technique for automatically verifying safety properties of concurrent programs, in particular programs which rely on subtle dependen- cies of local states of different threads, such as lock-free implementations of stacks and queues in an environment without garbage collection. Our technique addresses the joint challenges of infinite-state specifications, an unbounded num- ber of threads, and an unbounded heap managed by explicit memory allocation. Our technique builds on the automata-theoretic approach to model checking, in which a specification is given by an automaton that observes the execution of a program and accepts executions that violate the intended specification. We extend this approach by allowing specifications to be given by a class of infinite-state au- tomata. We show how such automata can be used to specify queues, stacks, and other data structures, by extending a data-independence argument. For verifica- tion, we develop a shape analysis, which tracks correlations between pairs of threads, and a novel abstraction to make the analysis practical. We have imple- mented our method and used it to verify programs, some of which have not been verified by any other automatic method before.
|
|
| 6. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Automatic fence insertion in integer programs via predicate abstraction
- 2012
-
In: Static Analysis. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642331244 - 9783642331251 ; , s. 164-180
-
Conference paper (peer-reviewed)abstract
- We propose an automatic fence insertion and verification framework for concurrent programs running under relaxed memory. Unlike previous approaches to this problem, which allow only variables of finite domain, we target programs with (unbounded) integer variables. The problem is difficult because it has two different sources of infiniteness: unbounded store buffers and unbounded integer variables. Our framework consists of three main components: (1) a finite abstraction technique for the store buffers, (2) a finite abstraction technique for the integer variables, and (3) a counterexample guided abstraction refinement loop of the model obtained from the combination of the two abstraction techniques. We have implemented a prototype based on the framework and run it successfully on all standard benchmarks together with several challenging examples that are beyond the applicability of existing methods.
|
|
| 7. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Counter-Example Guided Fence Insertion under TSO
- 2012
-
In: TACAS 2012. - Berlin, Heidelberg : Springer. - 9783642287558 - 9783642287565
-
Conference paper (peer-reviewed)abstract
- We give a sound and complete fence insertion procedure for concurrentfinite-state programs running under the classical TSO memory model. Thismodel allows “write to read” relaxation corresponding to the addition of an unboundedstore buffer between each processor and the main memory. We introducea novel machine model, called the Single-Buffer (SB) semantics, and show thatthe reachability problem for a program under TSO can be reduced to the reachabilityproblem under SB. We present a simple and effective backward reachabilityanalysis algorithm for the latter, and propose a counter-example guided fence insertionprocedure. The procedure is augmented by a placement constraint thatallows the user to choose places inside the program where fences may be inserted.For a given placement constraint, we automatically infer all minimal setsof fences that ensure correctness. We have implemented a prototype and run itsuccessfully on all standard benchmarks together with several challenging examplesthat are beyond the applicability of existing methods.
|
|
| 8. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO
- 2013
-
In: Tools and Algorithms for the Construction and Analysis of Systems. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642367410 - 9783642367427 ; , s. 530-536
-
Conference paper (peer-reviewed)abstract
- We introduce MEMORAX, a tool for the verification of control state reachability (i.e., safety properties) of concurrent programs manipulating finite range and integer variables and running on top of weak memory models. The verification task is non-trivial as it involves exploring state spaces of arbitrary or even infinite sizes. Even for programs that only manipulate finite range variables, the sizes of the store buffers could grow unboundedly, and hence the state spaces that need to be explored could be of infinite size. In addition, MEMORAX in- corporates an interpolation based CEGAR loop to make possible the verification of control state reachability for concurrent programs involving integer variables. The reachability procedure is used to automatically compute possible memory fence placements that guarantee the unreachability of bad control states under TSO. In fact, for programs only involving finite range variables and running on TSO, the fence insertion functionality is complete, i.e., it will find all minimal sets of memory fence placements (minimal in the sense that removing any fence would result in the reachability of the bad control states). This makes MEMORAX the first freely available, open source, push-button verification and fence insertion tool for programs running under TSO with integer variables.
|
|
| 9. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Verifying Safety and Liveness for the FlexTM Hybrid Transactional Memory
- 2013
-
In: <em>Design, Automation & Test in Europe (DATE 2013), Grenoble, France, March 18-22, 2013.</em>. - Grenoble, France : IEEE. - 9781467350716 ; , s. 785-790
-
Conference paper (peer-reviewed)abstract
- We consider the verification of safety (strict se- rializability and abort consistency) and liveness (obstruction and livelock freedom) for the hybrid transactional memory framework FLEXTM. This framework allows for flexible imple- mentations of transactional memories based on an adaptation of the MESI coherence protocol. FLEXTM allows for both eager and lazy conflict resolution strategies. Like in the case of Software Transactional Memories, the verification problem is not trivial as the number of concurrent transactions, their size, and the number of accessed shared variables cannot be a priori bounded. This complexity is exacerbated by aspects that are specific to hardware and hybrid transactional memories. Our work takes into account intricate behaviours such as cache line based conflict detection, false sharing, invisible reads or non-transactional instructions. We carry out the first automatic verification of a hybrid transactional memory and establish, by adopting a small model approach, challenging properties such as strict serializability, abort consistency, and obstruction freedom for both an eager and a lazy conflict resolution strategies. We also detect an example that refutes livelock freedom. To achieve this, our prototype tool makes use the latest antichain based techniques to handle systems with tens of thousands of states.
|
|
| 10. |
- Abelsson, J, et al.
(author)
-
The outcome of allo-HSCT for 92 patients with myelofibrosis in the Nordic countries.
- 2012
-
In: Bone Marrow Transplantation. - : Nature Publishing Group. - 0268-3369 .- 1476-5365. ; 47:3, s. 380-386
-
Journal article (peer-reviewed)abstract
- Between 1982 and 2009 a total of 92 patients with myelofibrosis (MF) in chronic phase underwent allo-SCT in nine Nordic transplant centers. Myeloablative conditioning (MAC) was given to 40 patients, and reduced intensity conditioning (RIC) was used in 52 patients. The mean age in the two groups at transplantation was 46±12 and 55±8 years, respectively (P<0.001). When adjustment for age differences was made, the survival of the patients treated with RIC was significantly better (P=0.003). Among the RIC patients, the survival was significantly (P=0.003) better for the patients with age <60 years (a 10-year survival close to 80%) than for the older patients. The type of stem cell donor did not significantly affect the survival. No significant difference was found in TRM at 100 days between the MAC- and the RIC-treated patients. The probability of survival at 5 years was 49% for the MAC-treated patients and 59% in the RIC group (P=0.125). Patients treated with RIC experienced significantly less aGVHD compared with patients treated with MAC (P<0.001). The OS at 5 years was 70, 59 and 41% for patients with Lille score 0, 1 and 2, respectively (P=0.038, when age adjustment was made). Twenty-one percent of the patients in the RIC group were given donor lymphocyte infusion because of incomplete donor chimerism, compared with none of the MAC-treated patients (P<0.002). Nine percent of the patients needed a second transplant because of graft failure, progressive disease or transformation to AML, with no significant difference between the groups. Our conclusions are (1) allo-SCT performed with RIC gives a better survival compared with MAC. (2) age over 60 years is strongly related to a worse outcome and (3) patients with higher Lille score had a shorter survival.
|
|
