Checking the correctness of complex concurrent programs is inherently challenging due to the large amount of code and complex structures. Three key issues are required to addressed: choosing a proper correctness condition as a goal of checking, proposing an effective approach for checking the correctness condition, and adapting the architectural details of complex concurrent programs. In this paper we propose an efficient methodology to address these issues by considering complex concurrent programs as concurrent objects. To solve the first issue, linearizability, a de facto correctness criterion for concurrent objects, is chosen as the correctness condition for complex concurrent programs. To solve the second issue, we propose an effective approach to reduce the potential exponential explosion in linearizability checking. Sequential executions are referred to as sequential specifications with their correctness guaranteed via a combination of a replay mechanism and the insertion of assertions. The third issue requires to solve architecture-relevant problems that hinder linearizability checking. We propose a notion called “macro operations” to assemble “fragments” of operations. This is quite suitable for dealing with inter-core interrupt mechanisms. To demonstrate the effectiveness of our methodology, we verify a task management and scheduling system, which is a critical component of a multi-core embedded operating system kernel, supporting the preemptive multi-core task scheduling and inter-core interrupts. During this process, we found and fixed numerous errors in the original system design, which were confirmed by the system developer.