Multithreaded concurrency is an extremely challenging programming setting, with bugs manifesting themselves in resource starvation and atomicity violations. While there have been efforts to simplify concurrent programming through higher-level programming abstractions, developers tend to choose low-level concurrent programming abstractions (with locks and condition variables as synchronization primitives) due to efficiency issues. This talk will present my recent work on bridging this efficiency vs. programmability trade-off in concurrent programming by employing lightweight formal methods in the compiler. Given a concurrent program implemented in a higher-level programming abstraction, our approach automatically synthesizes efficient and correct-by-construction code implemented in terms of standard synchronization primitives. Specifically, the first part of the talk will demonstrate how to synthesize all necessary signaling operations, and the second part will illustrate how to synthesize a fine-grained locking scheme that maximizes parallelism. As I will demonstrate through empirical results, this approach notably simplifies concurrent programming while achieving optimal performance.